Stainless Actors

[jad-hamza]

Since we've added checks to arguments aliasing https://github.com/epfl-lara/stainless/pull/965, the stainless actors fails because of aliasing here: https://github.com/epfl-lara/stainless-actors/blob/8173788e75880fa04d004cd8443ed0ef70b1cd83/examples/kvs/src/main/scala/KVS.scala#L67

There is aliasing between ctx.self and the implicit parameter ctx being passed to !: https://github.com/epfl-lara/stainless-actors/blob/8173788e75880fa04d004cd8443ed0ef70b1cd83/src/main/scala/Actors.scala#L25

[vkuncak]

Was this fixed in the benchmark, @jad-hamza ?

[jad-hamza]

No, we need to reorganize a bit the actors library to avoid the aliasing. The actors nightly tests are currently disabled from Stainless.

[mario-bucev]

I have tested them locally, it verifies. We could maybe try to enable them back (https://github.com/epfl-lara/stainless/pull/1208)?

[vkuncak]

We should see if we can pass mutable objects between actors by using array swap primitive or adding something analogous. Actors need to have a state, and this state can be used to emulate non-determinism of communication. This seems like the fastest path to some form of concurrency in Stainless.

[mario-bucev]

If I'm not mistaken, actors should exchange immutable messages, but they are (obviously) allowed to mutate their data.