Given two or more well-founded binary relations, when can one be certain that their union is likewise well-founded? We provide conditions for an arbitrary number of relations, generalizing known conditions for two relations, along with counterexamples to several potential weakenings. Such conditions may be useful for proving termination of rewrite …
read moreFrom Reo circuit to fast and safe Rust source
The Reo compiler is able to translate a textual protocol specification into source code in several target languages. Currently, low-level systems languages such as Rust are not supported. In addition to easy inter-operation with C and C++, Rust's strict type system allow for highly expressive APIs that give stronger safety …
read moreReproducible Simulations, Trace Visualization and Model Exploration with Dynamic Partial Order Reduction in Real-Time ABS
Local traces are our means for recording and (deterministically) replaying Real-Time ABS models. The traces capture communication between actors in a model, and a tool has been developed for visualizing them. From a given trace, we can generate new traces, that can be executed by the Real-Time ABS simulator; doing …
read moreFormalizing the Semantics of Concurrent Revisions
Concurrent revisions is a concurrency control model developed by Microsoft Research. It has many interesting properties that distinguish it from other well-known models such as transactional memory. One of these properties is determinacy: programs written within the model always produce the same outcome, independent of scheduling. The concurrent revisions model …
read moreYet Another Reo Semantics: Reasoning about Speculative Execution
Speculative execution is a well-known technique that allows for the optimization of concurrent systems. In this talk, we explore an extension to Reo that allows reasoning about speculations, and introduce a semantics based on a logical framework with data types and data streams. Our semantics has the capability to detect …
read moreNerve Nets, Omega-regular Languages, and Reo
In this talk we relate Reo to some fundamental results in computer science.
In 1951, S.C. Kleene detailed the construction of nerve nets, and characterized their behavior in terms of events occurring within a finite frame of time. He then proved that regular events are exactly the events generated …
read moreVerification of Distributed Epistemic Gossip Protocols
Gossip protocols are concerned with the spread of knowledge in a social network. They aim at arriving, by means of point-to-point or group communications, at a situation in which all agents know each other secrets.
We consider distributed gossip protocols that are expressed in a simple programming language that employs …
read moreA Scala Library for Actor-Based Cooperative Scheduling
Actor-based models of computation in general assume a run-to-completion mode of execution of the messages. The Abstract Behavioral Specification (ABS) Language extends the Actor-based model with a high-level synchronization mechanism which allows actors to suspend the execution of the current message and schedule in a cooperative manner another queued message …
read moreCompilation of Reo protocols
Reo is an interaction-centric model of concurrency for compositional specification of communication and coordination protocols. Recently, Jongmans developed techniques to compile Reo protocols into executable code. Benchmarks show that compilation of Reo protocols can produce code whose performance is comparable or even beats that of hand-crafted programs. Unfortunately, Jongmans' techniques …
read moreGossip In NetKAT
In this talk we will combine the study of NetKAT with the study of dynamic gossip. The talk is largely based on my master thesis, but as I am currently working on this will also contain some work in progress and loose ends. NetKAT is a sound and complete network …
read more