Din, Crystal Chang ; Owe, Olaf (2014)
A sound and complete reasoning system for asynchronous communication with shared futures.
In: Journal of Logical and Algebraic Methods in Programming, 83 (5-6)
doi: 10.1016/j.jlamp.2014.03.003
Artikel, Bibliographie
Kurzbeschreibung (Abstract)
Abstract Distributed and concurrent object-oriented systems are difficult to analyze due to the complexity of their concurrency, communication, and synchronization mechanisms. We consider the setting of concurrent objects communicating by asynchronous method calls. The future mechanism extends the traditional method call communication model by facilitating sharing of references to futures. By assigning method call result values to futures, third party objects may pick up these values. This may reduce the time spent waiting for replies in a distributed environment. However, futures add a level of complexity to program analysis, as the program semantics becomes more involved. This paper presents a Hoare style reasoning system for distributed objects based on a general concurrency and communication model focusing on asynchronous method calls and futures. The model facilitates invariant specifications over the locally visible communication history of each object. Compositional reasoning is supported, and each object may be specified and verified independently of its environment. The presented reasoning system is proven sound and (relatively) complete with respect to the given operational semantics.
| Typ des Eintrags: | Artikel |
|---|---|
| Erschienen: | 2014 |
| Autor(en): | Din, Crystal Chang ; Owe, Olaf |
| Art des Eintrags: | Bibliographie |
| Titel: | A sound and complete reasoning system for asynchronous communication with shared futures |
| Sprache: | Deutsch |
| Publikationsjahr: | 2014 |
| Titel der Zeitschrift, Zeitung oder Schriftenreihe: | Journal of Logical and Algebraic Methods in Programming |
| Jahrgang/Volume einer Zeitschrift: | 83 |
| (Heft-)Nummer: | 5-6 |
| DOI: | 10.1016/j.jlamp.2014.03.003 |
| Kurzbeschreibung (Abstract): | Abstract Distributed and concurrent object-oriented systems are difficult to analyze due to the complexity of their concurrency, communication, and synchronization mechanisms. We consider the setting of concurrent objects communicating by asynchronous method calls. The future mechanism extends the traditional method call communication model by facilitating sharing of references to futures. By assigning method call result values to futures, third party objects may pick up these values. This may reduce the time spent waiting for replies in a distributed environment. However, futures add a level of complexity to program analysis, as the program semantics becomes more involved. This paper presents a Hoare style reasoning system for distributed objects based on a general concurrency and communication model focusing on asynchronous method calls and futures. The model facilitates invariant specifications over the locally visible communication history of each object. Compositional reasoning is supported, and each object may be specified and verified independently of its environment. The presented reasoning system is proven sound and (relatively) complete with respect to the given operational semantics. |
| Freie Schlagworte: | Distributed systems, Compositional reasoning, Hoare Logic, Concurrent objects, Operational semantics, Communication history |
| ID-Nummer: | TUD-CS-2014-0997 |
| Fachbereich(e)/-gebiet(e): | 20 Fachbereich Informatik > Software Engineering 20 Fachbereich Informatik |
| Hinterlegungsdatum: | 31 Dez 2016 10:40 |
| Letzte Änderung: | 16 Mai 2018 12:06 |
| PPN: | |
| Export: | |
| Suche nach Titel in: | TUfind oder in Google |
 |
Frage zum Eintrag |
Optionen (nur für Redakteure)
 |
Redaktionelle Details anzeigen |
Drucken
Impressum