Name
Abstract | ||
|---|---|---|
This paper proposes a simple yet concise framework to statically verify communication correctness in a concurrency model using futures. We consider the concurrency model of the core ABS language, which supports actor-style asynchronous communication using futures and cooperative scheduling. We provide a type discipline based on session types, which gives a high-level abstraction for structured interactions. By using it we statically verify if the local implementations comply with the communication correctness. We extend core ABS with sessions and annotations to express scheduling policies based on required communication ordering. The annotation is statically checked against the session automata derived from the session types. |
Year | DOI | Venue |
|---|---|---|
2016 | 10.1007/978-3-319-47846-3_19 | Lecture Notes in Computer Science |
Field | DocType | Volume |
Asynchronous communication,Abstraction,Object type,Concurrency,Computer science,Futures contract,Scheduling (computing),Correctness,Automaton,Theoretical computer science | Conference | 10009 |
ISSN | Citations | PageRank |
0302-9743 | 4 | 0.42 |
References | Authors | |
11 | 3 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Eduard Kamburjan | 1 | 11 | 2.24 |
| Crystal Chang Din | 2 | 82 | 7.87 |
| Tzu-Chun Chen | 3 | 20 | 3.67 |