Makes .ok() use in forked scopes illegal

[lbialy]

Makes .ok() use in forked scopes illegal if not wrapped in either in forked scope.

Quite literally capture checker at home.

[Ichoran]

This is probably a good idea. Does the mechanism work if you can have nested either:, though?

[lbialy]

It does, check out the given't pattern with ambiguous instances removing given from a subsequent scope.

…

On Wed 5. Jun 2024 at 01:46, Ichoran ***@***.***> wrote: This is probably a good idea. Does the mechanism work if you can have nested either:, though? — Reply to this email directly, view it on GitHub <#146 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/ACBVNUSZVRCAPPNLXKJGPUDZFZGT7AVCNFSM6AAAAABIYT5LJKVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZDCNBYGU4DOOJSGQ> . You are receiving this because you authored the thread.Message ID: ***@***.***>

[adamw]

So the illegal situation that we want to prevent is:

supervised:
  either:
    fork:
      sth.ok()

as then the exception is thrown by the outer scope. However, we also prevent this one which is correct:

either:
  supervised:
    fork:
      sth.ok()

and should work just fine. Is that correct? Any other situations which would be ruled out by the change?

Also, this is illegal as well, but would compile just fine I suppose, as we're capturing the capability at a different place:

supervised:
  either:
    def x = sth.ok()
    fork(x)

Another variants would be disallowing of running fork if there's a Label in scope (also using NotGiven), or disallowing either if there's an Ox in scope. Maybe these would catch a wider array of bugs ... or maybe they would be too restrictive. Did you consider these?

[lbialy]

Yeah, regarding the last one - that's impossible to do without capture calculus afaik. The second one surprised me a bit, I didn't expect it to be valid but it it, just as .ok() is fine in mapPar, because both supervised and mapPar rethrows correctly. Let me reformulate this PR.

[lbialy]

@prolativ could you take a look at this:

[warn] -- [E129] Potential Issue Warning: /Users/lbialy-tv/Projects/ox/core/src/test/scala/ox/ForkEitherInteropTest.scala:194:16
[warn] 194 |          sth.ok()
[warn]     |          ^^^^^^^^
[warn]     |A pure expression does nothing in statement position; you may be omitting necessary parentheses
[warn]     |---------------------------------------------------------------------------
[warn]     |Inline stack trace
[warn]     |- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
[warn]     |This location contains code that was inlined from either.scala:57
[warn]  57 |      inline if availableInScope[Forked] && !availableInScope[Supervised] then
[warn]     |      ^
[warn]  58 |        error(
[warn]  59 |          "This use of .ok() belongs to either block outside of the fork and is therefore illegal. Use either block inside of the forked block."
[warn]  60 |        )
[warn]      ---------------------------------------------------------------------------
[warn]     |---------------------------------------------------------------------------
[warn]     | Explanation (enabled by `-explain`)
[warn]     |- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
[warn]     | The pure expression inline if
[warn]     |   ox.either.availableInScope[ox.Forked].&&(
[warn]     |     ox.either.availableInScope[ox.Supervised].unary_!)
[warn]     |  then
[warn]     |   scala.compiletime.error(
[warn]     |
[warn]     |       "This use of .ok() belongs to either block outside of the fork and is therefore illegal. Use either block inside of the forked block."
[warn]     |
[warn]     |   )
[warn]     |  else () doesn't have any side effect and its result is not assigned elsewhere.
[warn]     | It can be removed without changing the semantics of the program. This may indicate an error.
[warn]      ---------------------------------------------------------------------------

It's triggered by this piece of code:

    transparent inline def ok(): A =
      inline if availableInScope[Forked] && !availableInScope[Supervised] then
        error(
          "This use of .ok() belongs to either block outside of the fork and is therefore illegal. Use either block inside of the forked block."
        )

I think it's mistaken, it's not a pure expression per se, it stops compilation if something is borked. No idea how to suppress it with @nowarn.

[prolativ]

@lbialy the compiler's warning is quite misleading. It seems that the problem is that error(...) returns Nothing rather than Unit. When .ok() is being inlined and the conditions for the error are fulfilled, sth.ok() gets replaced with something like

{
  error(...) // non-Unit expression in non-returning position 
  summonFrom { ... }
}

The fix seems to be to change the implementation of ok from

inline if ... then
  error(...)
summonFrom { ... }

to

inline if ... then
  error(...)
else
  summonFrom { ... }

[lbialy]

Interesting! I tried adding () as the last thing in both inline if branches and that didn't do the trick. Thanks!

…

On Thu 13. Jun 2024 at 10:18, Michał Pałka ***@***.***> wrote: @lbialy <https://github.com/lbialy> the compiler's warning is quite misleading. It seems that the problem is that error(...) returns Nothing rather than Unit. When .ok() is being inlined and the conditions for the error are fulfilled, sth.ok() gets replaced with something like { error(...) // non-Unit expression in non-returning position summonFrom { ... } } The fix seems to be to change the implementation of ok from inline if ... then error(...) summonFrom { ... } to inline if ... then error(...)else summonFrom { ... } — Reply to this email directly, view it on GitHub <#146 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/ACBVNUXEGEBZYQSTB6LZGQTZHFIVTAVCNFSM6AAAAABIYT5LJKVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZDCNRUHE3DAMJQHE> . You are receiving this because you were mentioned.Message ID: ***@***.***>

[lbialy]

This thing is still a bit WIP as @prolativ found a variant that is still borked:

[info] - should fail to compile invalid examples *** FAILED ***
[info]   Expected a compiler error, but got none for code:
[info]          import ox.*
[info]          import ox.either.*
[info]
[info]          supervised { 
[info]            either { 
[info]              fork { 
[info]                supervised { 
[info]                  Right(1).ok() // if forked && !supervised then error but it is forked and then supervised
[info]                }
[info]              }
[info]            }
[info]          }

trying to find a solution :/

[Ichoran]

I think the solution is to provide a fork depth implicit at every unbreakable boundary (incrementing the depth by one if you already are in an unbreakable boundary), then have either or any such block provide not a Label but an opaque type that wraps Label with the fork depth. You then ask that deeper fork depths are NotFound when you unwrap the opaque type to get your Label back.

I prototyped part of this far enough to convince myself that it works. I'm not sure I want to decorate my stuff with all this, however. There are a lot of things that can go wrong across thread boundaries (c.f. spores vs closures), and given that I'm going to be paranoid about it anyway, not jumping across the boundaries doesn't seem like the worst thing ever.

[Ichoran]

@lbialy - The same solution could be reused to avoid nested eithers: you look for any instance of the opaque type wrapping a label that has the depth that you read from the environment. Unless such a label is NotFound, you complain that you're nested.

So there are two interwoven implicits: thread boundaries define ForkDepth[D <: Int & Singleton] = Unit or somesuch, while either: creates a LabelLevel[A, N <: Int & Singleton] = Label[A].

Upon creating a new thread boundary, you summonFrom ForkDepth and either give a ForkDepth[1] if you're not inside one, or ForkDepth[D+1] if there is one. Upon creating a new either block, you label it with your ForkDepth, or 0 if you're not in a fork. To jump out, you summonFrom the ForkDepth and only if it matches your LabelLevel do you execute the jump by unpacking the Label.

This also prevents people from thwarting the safeguards by using boundary.break directly: it can't see that the LabelLevel is a Label.

[Ichoran]

@lbialy - I have a fully working nearly-zero-overhead prototype solution at https://github.com/Ichoran/kse3/blob/v0.3.3/basics/src/Abstractions.scala#L133-L166

(The Int & Singleton thing ended up being a drag because compiletime.ops.int doesn't respect the Singleton property, so I used a different strategy.)

This replaces the boundary/break abstraction with a hop.here/Corral/Hop.jump abstraction, where a jump cannot penetrate a corral. (I'll probably rename here from; better semantics in some ways.)

@prolativ - I think that by using this abstraction, the desired functionality can be implemented without any of the problems you found.

Here is a scala-cli runnable example:

//> using scala 3.4.2
//> using dep com.github.ichoran::kse3-basics:0.3.3
//> using mainClass lab.kerrr.examples.hopcorral.Main
//> using options -deprecation -Wconf:msg=is.not.declared.infix:s

package lab.kerrr.examples.hopcorral

import kse.basics.*

object Main {
  def doesNotCompile(): Boolean = compiletime.testing.typeChecks("""
    hop[Int].here:
      Corral:
        hop[String].here:
          Hop.jump(5)
          Hop.jump("eel")
          "cod"
      2
  """)
  
  def doesCompile1(): Int =
    hop[Int].here:
      Corral:
        hop[String].here:
          Hop.jump("salmon")
          "eel"
      .length
  
  def doesCompile2(): Int =
    Corral:
      hop[Int].here:
        hop[String].here:
          Hop.jump(5)
          Hop.jump("eel")
          "cod"
        2

  def main(args: Array[String]): Unit =
    println(s"Jump escapes corral: ${doesNotCompile()}")
    println(s"Jump within corral yields ${doesCompile1()}")
    println(s"Longer jump within corral yields ${doesCompile2()}")
}

[lbialy]

Wow, cool example @Ichoran! I've been discussing this with @prolativ and he has another idea with givens with flags for granular control but it requires dynamic creation of givens so it's a bit more heavy and currently doesn't work with the given't pattern so it would require a full overhaul of capabilities in ox :( I'll try to understand your Corral thing though.

Btw.: I've pushed our tests and you can see how many variants are possible. Current solution fails only one.

[lbialy]

@Ichoran I don't think this solution with singletons will work in structured concurrency setup where we have different boundaries that introduce different semantics and allow different contents. Specifically, I don't see a way for this to work with:

 either:
   supervised:
     fork:
       Right(1).ok()

which is the main pain point @adamw mentioned - supervised does wait for all forks and rethrows so this is a valid syntax where we have a get-away application of .ok() combinator but it's fine, because should it fail - it will all roll-up to the initial either block. The problematic case that's currently blocking this PR is:

supervised:
  either:
    fork:
      supervised: 
        Right(1).ok()

where outer supervised provides Ox capability for fork so that compiles, there's an either block inside of the outer supervised which is a big no-no as forks are not throwing and should the fork fail the outer supervised will rethrow. Then there's a fork scope and another supervised scope that breaks the checks done in .ok() combinator on this branch which makes the code compile. If either: was providing your Singleton-augmented opaque Hop type and fork: provided the Corral[S], it would prevent the valid first case.

[Ichoran]

@lbialy - Fair enough; you would need a corral that you can get through in that case. If fork increases the corral depth, but supervised memoizes the current corral depth (e.g. Corral[C] => Gate[C]), and ok() checks that the target corral depth is either below the supervised depth or at least the fork depth, it should work.

It's getting to be a lot of machinery at that point, however. A simpler way would be nice, if you can find it.

The key observation, though, is that it's very difficult to effectively remove things from scope, so using an add-and-compare strategy is better.

[lbialy]

Removal through given't works pretty well. Problem is that it interacts with implicits based on presence of other implicits and that's how we approached this last problem.

[Ichoran]

That's what I mean by "difficult to effectively remove things from scope". It's not precisely the same as having a set of contexts and removing one context from the set, and being not-precisely-the-same causes difficulty.

[Ichoran]

@lbialy - The bytecode is a lot worse with corrals as I've implemented them. Two boundaries and two jumps add about 150 bytes of bytecode, plus primitives box when they don't need to, and a Label object is instantiated despite it being unneeded. There's no reason it ought to be the case, but at least until erased hits, this could be a performance hit.

[Ichoran]

This won't really work without any overhead until erased is in and non-experimental (and works with context functions), but I got it down to about 70-80 bytes extra and no boxing.

[Ichoran]

The witness-only (not opaque Label) version of Hop is here: https://github.com/Ichoran/kse3/blob/359c4e8fd1476db46ac060b8277745e3ca2718c8/basics/src/Abstractions.scala#L143-L163

[adamw]

This is some impressive work, but in the end, I'm afraid the machinery involved doesn't carry its weight.
We want to prevent a single scenario, if I'm not mistaken: either - fork - .ok(), ran within a concurrency scope (so within a supervised or when using Ox is available).
To achieve that, we introduce a couple of new pseudo-capabilities, which are visible in the signatures, but not really designed to be used by users (e.g. in user-land method signatures). It's great to have this researched, but I would be weary of complicating Ox just to prevent such situations. As an alternative, we can always try education, that is: clearly documenting the limitations of our design, or trying turning .ok into a macro which inspects its surroundings.