Conference proceeding
Modal Assertions for Actor Correctness
PROCEEDINGS OF THE 9TH ACM SIGPLAN INTERNATIONAL WORKSHOP ON PROGRAMMING BASED ON ACTORS, AGENTS, AND DECENTRALIZED CONTROL (AGERE '19)
01 Jan 2019
Featured in Collection : UN Sustainable Development Goals @ Drexel
Abstract
The actor model is a well-established way to approach to modularly designing and implementing concurrent and/or distributed systems, seeing increasing adoption in industry. But deductive verification tailored to actor programs remains underexplored; general concurrent logics could be used, but the logics are complex and full of features to reason about behaviors the actor model strives to avoid.
We explore a relatively lightweight approach of extending a system for proving sequential program correctness with means to prove safety properties of actor programs (currently, assuming no faults). We borrow ideas from hybrid logic, a modal logic for stating assertions are true at a particular point in a model (in this case, a particular actor's local state). To make such assertions useful, we stabilize them using rely-guarantee-style reasoning over local actor states, and only permit sending stable versions of these assertions to other actors. By carefully restricting the formation of assertions that a proposition is true at a certain actor, we avoid the need for actors to handle each others' rely-guarantee relations explicitly. Finally, we argue that the approach requires only modest adjustments beyond applying traditional sequential techniques to actors with immutable messages, by implementing most of the logic as a Dafny library.
Metrics
Details
- Title
- Modal Assertions for Actor Correctness
- Creators
- Colin S. Gordon - Drexel University
- Contributors
- F Bergenti (Editor)E Castegren (Editor)J DeKoster (Editor)J Franco (Editor)
- Publication Details
- PROCEEDINGS OF THE 9TH ACM SIGPLAN INTERNATIONAL WORKSHOP ON PROGRAMMING BASED ON ACTORS, AGENTS, AND DECENTRALIZED CONTROL (AGERE '19)
- Conference
- 9TH ACM SIGPLAN INTERNATIONAL WORKSHOP ON PROGRAMMING BASED ON ACTORS, AGENTS, AND DECENTRALIZED CONTROL (AGERE '19), 9th
- Publisher
- Assoc Computing Machinery
- Number of pages
- 10
- Grant note
- CCF-1844964 / National Science Foundation; National Science Foundation (NSF)
- Resource Type
- Conference proceeding
- Language
- English
- Academic Unit
- Computer Science
- Web of Science ID
- WOS:000775702500002
- Scopus ID
- 2-s2.0-85076772315
- Other Identifier
- 991019168457804721
UN Sustainable Development Goals (SDGs)
This publication has contributed to the advancement of the following goals:
InCites Highlights
Data related to this publication, from InCites Benchmarking & Analytics tool:
- Web of Science research areas
- Computer Science, Software Engineering
- Computer Science, Theory & Methods