Making weak memory models fair

Liveness properties, such as termination, of even the simplest shared-memory concurrent programs under sequential consistency typically require some fairness assumptions about the scheduler. Under weak memory models, we observe that the standard notions of thread fairness are insufficient, and an additional fairness property, which we call memory fairness, is needed. In this paper, we propose a uniform definition for memory fairness that can be integrated into any declarative memory model enforcing acyclicity of the union of the program order and the reads-from relation. For the well-known models, SC, x86-TSO, RA, and StrongCOH, that have equivalent operational and declarative presentations, we show that our declarative memory fairness condition is equivalent to an intuitive model-specific operational notion of memory fairness, which requires the memory system to fairly execute its internal propagation steps. Our fairness condition preserves the correctness of local transformations and the compilation scheme from RC11 to x86-TSO, and also enables the first formal proofs of termination of mutual exclusion lock implementations under declarative weak memory models.

Propositions-as-types and shared state

We develop a principled integration of shared mutable state into a proposition-as-types linear logic interpretation of a session-based concurrent programming language. While the foundation of type systems for the functional core of programming languages often builds on the proposition-as-types correspondence, automatically ensuring strong safety and liveness properties, imperative features have mostly been handled by extra-logical constructions. Our system crucially builds on the integration of nondeterminism and sharing, inspired by logical rules of differential linear logic, and ensures session fidelity, progress, confluence and normalisation, while being able to handle first-class shareable reference cells storing any persistent object. We also show how preservation and, perhaps surprisingly, progress, resiliently survive in a natural extension of our language with first-class locks. We illustrate the expressiveness of our language with examples highlighting detailed features, up to simple shareable concurrent ADTs.

Cross-chain deals and adversarial commerce

Modern distributed data management systems face a new challenge: how can autonomous, mutually distrusting parties cooperate safely and effectively? Addressing this challenge brings up familiar questions from classical distributed systems: how to combine multiple steps into a single atomic action, how to recover from failures, and how to synchronize concurrent access to data. Nevertheless, each of these issues requires rethinking when participants are autonomous and potentially adversarial. We propose the notion of a cross-chain deal, a new way to structure complex distributed computations that manage assets in an adversarial setting. Deals are inspired by classical atomic transactions, but are necessarily different, in important ways, to accommodate the decentralized and untrusting nature of the exchange. We describe novel safety and liveness properties, along with two alternative protocols for implementing cross-chain deals in a system of independent blockchain ledgers. One protocol, based on synchronous communication, is fully decentralized, while the other, based on semi-synchronous communication, requires a globally shared ledger. We also prove that some degree of centralization is required in the semi-synchronous communication model.

Formal Modeling, Proving, and Model Checking of a Flood Warning, Monitoring, and Rescue System-of-Systems

Floods after monsoon rains are frequent disasters that affect millions of lives in Pakistan. Human lives are lost, agriculture economies are destroyed, and livestock animals, houses, fruit farms, and crops are lost which are the major livelihoods of thousands of people in Punjab. Each year there are heavy rains in the monsoon season and, due to global warming, there is the rapid melting of snow in northern glaciers; these factors subsequently cause floods. There is also loss of life due to the spread of waterborne diseases and snake bites. Flood monitoring provides early detection of a flood and the calculation of its intensity, which results in reduced human life losses and economic losses. Most casualties are caused by the lack of timely real-time, authentic information about the high-risk areas, and flood intensity, speed, and direction. Therefore, the proposed approach is centered on formal modeling and verification of safety and liveness properties of flood monitoring perceivers. Each flood perceiver has several sensors. It requires the collection of information starting from the flood perceiver, observer, and environmental forecast. This information is processed to determine the flood intensity level. We have developed a CP-Nets’ formal model and model-checked it. We have verified the safety and liveness properties of correctness by exhaustive verification of the system using model-based proof obligations (Event-B method using Rodin). Our objective in this research is to propose a correct, reliable, and efficient flood warning, monitoring, and rescue (WMR) SoS based on formal methods. We have used formal modeling and model-checking based on state-of-the-art hierarchical CP-Nets supported by exhaustive formal proof obligations of Event-B.

An axiomatic approach to existence and liveness for differential equations

This article presents an axiomatic approach for deductive verification of existence and liveness for ordinary differential equations (ODEs) with differential dynamic logic (dL). The approach yields proofs that the solution of a given ODE exists long enough to reach a given target region without leaving a given evolution domain. Numerous subtleties complicate the generalization of discrete liveness verification techniques, such as loop variants, to the continuous setting. For example, ODE solutions may blow up in finite time or their progress towards the goal may converge to zero. These subtleties are handled in dL by successively refining ODE liveness properties using ODE invariance properties which have a complete axiomatization. This approach is widely applicable: several liveness arguments from the literature are surveyed and derived as special instances of axiomatic refinement in dL. These derivations also correct several soundness errors in the surveyed literature, which further highlights the subtlety of ODE liveness reasoning and the utility of an axiomatic approach. An important special case of this approach deduces (global) existence properties of ODEs, which are a fundamental part of every ODE liveness argument. Thus, all generalizations of existence properties and their proofs immediately lead to corresponding generalizations of ODE liveness arguments. Overall, the resulting library of common refinement steps enables both the sound development and justification of new ODE existence and of liveness proof rules from dL axioms. These insights are put into practice through an implementation of ODE liveness proofs in the KeYmaera X theorem prover for hybrid systems.

Temporal Refinements for Guarded Recursive Types

We propose a logic for temporal properties of higher-order programs that handle infinite objects like streams or infinite trees, represented via coinductive types. Specifications of programs use safety and liveness properties. Programs can then be proven to satisfy their specification in a compositional way, our logic being based on a type system.The logic is presented as a refinement type system over the guarded $$\lambda $$ λ -calculus, a $$\lambda $$ λ -calculus with guarded recursive types. The refinements are formulae of a modal $$\mu $$ μ -calculus which embeds usual temporal modal logics such as and . The semantics of our system is given within a rich structure, the topos of trees, in which we build a realizability model of the temporal refinement type system.

Model Checking $$\omega $$-Regular Properties with Decoupled Search

Decoupled search is a state space search method originally introduced in AI Planning. Similar to partial-order reduction methods, decoupled search exploits the independence of components to tackle the state explosion problem. Similar to symbolic representations, it does not construct the explicit state space, but sets of states are represented in a compact manner, exploiting component independence. Given the success of both partial-order reduction and symbolic representations when model checking liveness properties, our goal is to add decoupled search to the toolset of liveness checking methods. Specifically, we show how decoupled search can be applied to liveness verification for composed Büchi automata by adapting, and showing correct, a standard algorithm for detecting lassos (i.e., infinite accepting runs), namely nested depth-first search. We evaluate our approach using a prototype implementation.