Verifying fine-grained optimistic concurrent programs remains an open problem. Modern program logics provide abstraction mechanisms and compositional reasoning principles to deal with the inherent complexity. However, their use is mostly confined to pencil-and-paper or mechanized proofs. We devise a new separation logic geared towards the lacking automation. While local reasoning is known to be crucial for automation, we are the first to show how to retain this locality for (i) reasoning about inductive properties without the need for ghost code, and (ii) reasoning about computation histories in hindsight. We implemented our new logic in a tool and used it to automatically verify challenging concurrent search structures that require inductive properties and hindsight reasoning, such as the Harris set.
more »
« less
Modal assertions for actor correctness
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.
more »
« less
- Award ID(s):
- 1844964
- NSF-PAR ID:
- 10124073
- Date Published:
- Journal Name:
- Proceedings of the 9th ACM SIGPLAN International Workshop on Programming Based on Actors, Agents, and Decentralized Control
- Page Range / eLocation ID:
- 11 to 20
- Format(s):
- Medium: X
- Sponsoring Org:
- National Science Foundation
More Like this
-
-
more » « less
Formal verification of cyber-physical systems (CPS) is challenging because it has to consider real-time and concurrency aspects that are often absent in ordinary software. Moreover, the software in CPS is often complex and low-level, making it hard to assure that a formal model of the system used for verification is a faithful representation of the actual implementation, which can undermine the value of a verification result. To address this problem, we propose a methodology for building verifiable CPS based on the principle that a formal model of the software can be derived
automatically from its implementation. Our approach requires that the system implementation is specified inLingua Franca (LF), a polyglot coordination language tailored for real-time, concurrent CPS, which we made amenable to the specification of safety properties via annotations in the code. The program structure and the deterministic semantics of LF enable automatic construction of formal axiomatic models directly from LF programs. The generated models are automatically checked using Bounded Model Checking (BMC) by the verification engineUclid5 using theZ3 SMT solver. The proposed technique enables checking a well-defined fragment of Safety Metric Temporal Logic (Safety MTL) formulas. To ensure the completeness of BMC, we present a method to derive an upper bound on the completeness threshold of an axiomatic model based on the semantics of LF. We implement our approach in the LF Verifier and evaluate it using a benchmark suite with 22 programs sampled from real-life applications and benchmarks for Erlang, Lustre, actor-oriented languages, and RTOSes. The LF Verifier correctly checks 21 out of 22 programs automatically. -
Collaborative text editing applications like Google docs, Etherpad and Overleaf allow users to con- currently edit a “shared” document. Most existing collab- orative text editing software require total ordering on the updates made to the document, which is achieved using a centralized sever or some form of consensus algorithm. Then on top of the ordering, the editor uses either opera- tional transformation (OT) or differential synchronization (diff-sync) to apply the ordered update events to the already committed changes on their local copies. If there is no delay or failure, then eventually all updates can be applied correctly in the agreed order. Unfortunately, not only are these methods computation- ally intensive but they often result in conflicts due to users writing to the same location. It has also been proved that the metadata overhead for such protocols are at least linear in the number of delete events. Moreover, these event- based and diff-based algorithms are exceptionally difficult to implement and there are no provably correct solutions to these problems in the face of heavy concurrency. These collaborative editors either provide no proven guarantees or only provide eventual guarantees for correctness. With LiteDoc, we propose a different approach to tackle this problem: we make collaborative editing fast, scalable and robust by providing simplified semantics. More im- portantly, we can formally prove that LiteDoc achieves deterministic guarantees of correctness. LiteDoc divides the shared document into several sections and allow only one user to write at a particular section at any given time. This removes all conflicts that arise from having multiple writers writing to the same location. This mechanism also obviates the task of implementing cumbersome modules for OT, diff-sync and rollbacks in case of conflicts. Note that while LiteDoc supports less features than general collaborative editors like Google docs, it is natural (and courteous) to avoid concurrent writing to the same location when multiple people collaborate.more » « less
-
null (Ed.)Absatract Actors collaborate via message exchanges to reach a common goal. Experience has shown, however, that pure message-based communication is limiting and forces developers to use design patterns. The recently introduced dataspace actor model borrows ideas from the tuple space realm. It offers a tightly controlled, shared storage facility for groups of actors. In this model, actors assert facts that they wish to share and interests in such assertions. The dataspace notifies interested parties of changes to the set of assertions that they are interested in. Although it is straightforward to add the dataspace model to untyped languages, adding a typed interface is both necessary and challenging. Without restrictions on exchanged data, a faulty actor may propagate erroneous data through a malformed assertion, causing an otherwise well-behaved actor to crash—violating the key principle of failure isolation. A properly designed type system can prevent this scenario and rule out other kinds of uncooperative actors. This paper presents the first structural type system for the dataspace model of actors; it does not address the question of behavioral types for assertion-oriented protocols.more » « less
-
Probabilistic couplings are the foundation for many probabilistic relational program logics and arise when relating random sampling statements across two programs. In relational program logics, this manifests as dedicated coupling rules that, e.g., say we may reason as if two sampling statements return the same value. However, this approach fundamentally requires aligning or synchronizing the sampling statements of the two programs which is not always possible.more » « less
In this paper, we develop Clutch, a higher-order probabilistic relational separation logic that addresses this issue by supporting asynchronous probabilistic couplings. We use Clutch to develop a logical step-indexed logical relation to reason about contextual refinement and equivalence of higher-order programs written in a rich language with a probabilistic choice operator, higher-order local state, and impredicative polymorphism. Finally, we demonstrate our approach on a number of case studies.
All the results that appear in the paper have been formalized in the Coq proof assistant using the Coquelicot library and the Iris separation logic framework.
- Free Publicly Accessible Full Text
-
Accepted Manuscript1.0
- Conference Paper:
- https://doi.org/10.1145/3358499.3361221
