Name
Abstract | ||
|---|---|---|
We study deadlock detection in an actor model with wait-by-necessity synchronizations, a lightweight technique that synchronizes invocations when the corresponding values are strictly needed. This approach relies on the use of futures that are not given an explicit \"Future\" type. The approach we adopt explicits the synchronization on futures, and on the availability of some values, instead of the synchronization on the termination of a process existing in previous works. This way we are able to analyse the data-flow synchronization inherent to languages that feature wait-by-necessity. We provide a type-system and a solver inferring the type of a program so that deadlocks can be identified statically. As a consequence we can automatically verify the absence of deadlocks in actor programs with wait-by-necessity synchronizations. |
Year | DOI | Venue |
|---|---|---|
2016 | 10.1145/2967973.2968599 | PPDP |
Keywords | Field | DocType |
Deadlock detection, type system, behavioral types | Synchronization,Programming language,Computer science,Futures contract,Deadlock,Deadlock prevention algorithms,Solver,Actor model,Distributed computing | Conference |
Citations | PageRank | References |
5 | 0.51 | 13 |
Authors | ||
4 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Elena Giachino | 1 | 232 | 15.54 |
| Ludovic Henrio | 2 | 304 | 34.43 |
| Cosimo Laneve | 3 | 1035 | 83.41 |
| Vincenzo Mastandrea | 4 | 5 | 0.51 |