search

epfl-lara / stainless

Verification framework and tool for higher-order Scala programs
https://epfl-lara.github.io/stainless/
Apache License 2.0
356 stars 51 forks source link

Stainless Actors #970

Open jad-hamza opened 3 years ago

jad-hamza commented 3 years ago

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 commented 3 years ago

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

jad-hamza commented 3 years ago

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 commented 2 years ago

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

vkuncak commented 2 years ago

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 commented 2 years ago

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