survey of projects using Sala actors

Thomas Wies wrote:
>
> Dear all,
>
> in the context of a research initiative at EPFL we are developing a tool
> for
> static analysis and verification of Scala programs that use the Actor
> library. In particular, we are aiming at the verification of properties
> such
> as absence of deadlocks.
>
> We are currently making a survey of existing projects that use the Scala
> actor
> library, in order to collect some interesting benchmarks for our tool. If
> you
> are involved in or know of such a project whose source code could be made
> available to us, we would be happy to hear from you.
>
> Regards,
>
> Thomas Wies
>
>

The scala API for Fly (http://www.flyobjectspace.com/) makes use of actors.
I would be happy to be involved in this project if I can.

Channing

Thomas,

i would be very interested in what you plan to do here. i tried many times to get the existing actor semantics nailed down, but couldn't.

You probably already know that Luis Caires' spatial-behavioral types are a great starting point for doing what you're suggesting and the whole session-types cottage industry is also a reasonable starting point. (Personally, i would shy away from the Kobayashi types and TyPiCal.) However, without nailing down some things about the scheduling semantics there is no way to make the guarantees coming from the types actually apply to typed coded.

Moreover, you really, really can't call these things actors without specifying the notion of fairness at play. This is more than just a theoretical concern. Further, fairness and bisimulation-based arguments (that support the typing regimes) are closely connected.

It would be totally awesome to get an SOS specification for Scala actor semantics.

If you guys want an extra pair of hands on this, give me a shout. i'd love to pitch in. Ever since we did Enabled-Sets for Actor mailboxes in Rosette i've been dreaming about types for concurrency for a mainstream language.

Best wishes,

--greg

On Tue, Feb 10, 2009 at 8:10 AM, Thomas Wies <thomas.wies@epfl.ch> wrote:

Dear all,

in the context of a research initiative at EPFL we are developing a tool for
static analysis and verification of Scala programs that use the Actor
library. In particular, we are aiming at the verification of properties such
as absence of deadlocks.

We are currently making a survey of existing projects that use the Scala actor
library, in order to collect some interesting benchmarks for our tool. If you
are involved in or know of such a project whose source code could be made
available to us, we would be happy to hear from you.

Regards,

Thomas Wies

--
L.G. Meredith
Managing Partner
Biosimilarity LLC
806 55th St NE
Seattle, WA 98105

+1 206.650.3740

http://biosimilarity.blogspot.com