An official website of the United States government
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
This content will become publicly available on September 25, 2026
Actor Capabilities for Message Ordering
Not AvailableActor systems are a flexible model of concurrent and distributed programming, which are efficiently implementable, and avoid many classic concurrency bugs by construction. However they must still deal with the challenge of messages arriving in unexpected orders. We describe an approach to restricting the orders in which actors send messages to each other, by equipping actor references—the handle used to address another actor—with a protocol restricting which message types can be sent to another actor and in which order using that particular actor reference. This endows the actor references with the properties of (flow-sensitive) static capabilities, which we call actor capabilities. By sending other actors only restricted actor references, actors may control which messages are sent in which orders by other actors. Rules for duplicating (splitting) actor references ensure that these restrictions apply even in the presence of delegation. The capabilities themselves restrict message send ordering, which may form the foundation for stronger forms of reasoning. We demonstrate this by layering an effect system over the base type system, where the relationships enforced between the actor capabilities and the effects of an actor’s behaviour ensure that an actor’s behaviour is always prepared to handle any message that may arrive.
more »
« less
- Award ID(s):
- 2007582
- PAR ID:
- 10640813
- Publisher / Repository:
- Springer Nature Switzerland
- Date Published:
- Page Range / eLocation ID:
- 60 to 80
- Format(s):
- Medium: X
- Sponsoring Org:
- National Science Foundation
More Like this
-
-
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
-
Advancement in communication technologies and the Internet of Things (IoT) is driving adoption in smart cities that aims to increase operational efficiency and improve the quality of services and citizen welfare, among other potential benefits. The privacy, reliability, and integrity of communications must be ensured so that actions can be appropriate, safe, accurate, and implemented promptly after receiving actionable information. In this work, we present a multi-tier methodology consisting of an authentication and trust-building/distribution framework designed to ensure the safety and validity of the information exchanged in the system. Blockchain protocols and Radio Frequency-Distinct Native Attributes (RF-DNA) combine to provide a hardware-software codesigned system for enhanced device identity and overall system trustworthiness. Our threat model accounts for counterfeiting, breakout fraud, and bad mouthing of one entity by others. Entity trust (e.g., IoT devices) depends on quality and level of participation, quality of messages, lifetime of a given entity in the system, and the number of known "bad" (non-consensus) messages sent by that entity. Based on this approach to trust, we are able to adjust trust upward and downward as a function of real-time and past behavior, providing other participants with a trust value upon which to judge information from and interactions with the given entity. This approach thereby reduces the potential for manipulation of an IoT system by a bad or byzantine actor.more » « less
-
Elsman, Martin (Ed.)Protocols to ensure that messages are delivered in causal order are a ubiquitous building block of distributed systems. For instance, distributed data storage systems can use causally ordered message delivery to ensure causal consistency, and CRDTs can rely on the existence of an underlying causally-ordered messaging layer to simplify their implementation. A causal delivery protocol ensures that when a message is delivered to a process, any causally preceding messages sent to the same process have already been delivered to it. While causal delivery protocols are widely used, verification of their correctness is less common, much less machine-checked proofs about executable implementations. We implemented a standard causal broadcast protocol in Haskell and used the Liquid Haskell solver-aided verification system to express and mechanically prove that messages will never be delivered to a process in an order that violates causality. We express this property using refinement types and prove that it holds of our implementation, taking advantage of Liquid Haskell’s underlying SMT solver to automate parts of the proof and using its manual theorem-proving features for the rest. We then put our verified causal broadcast implementation to work as the foundation of a distributed key-value store.more » « less
-
Abstract Recent demand for distributed software had led to a surge in popularity in actor‐based frameworks. However, even with the stylized message passing model of actors, writing correct distributed software is still difficult. We present our work on linearizability checking in DS2, an integrated framework for specifying, synthesizing, and testing distributed actor systems. The key insight of our approach is that often subcomponents of distributed actor systems represent common algorithms or data structures (e.g., a distributed hash table or tree) that can be validated against a simple sequential model of the system. This makes it easy for developers to validate their concurrent actor systems without complex specifications. DS2 automatically explores the concurrent schedules that system could arrive at, and it compares observed output of the system to ensure it is equivalent to what the sequential implementation could have produced. We describe DS2's linearizability checking and test it on several concurrent replication algorithms from the literature. We explore in detail how different algorithms for enumerating the model schedule space fare in finding bugs in actor systems, and we present our own refinements on algorithms for exploring actor system schedules that we show are effective in finding bugs.more » « less
