More Like this

1. Independence and Causality in the Reversible Concurrent Setting

   https://doi.org/10.1007/978-3-031-97063-4_2  

   Aubert, Clément; Phillips, Iain; Ulidowski, Irek (June 2025, Springer Nature Switzerland)

   Glück, Robert; Kaarsgaard, Robin (Ed.)

   Among the formalisms that can be used to reason about concurrent systems, process calculi stand out both for their simple syntax and close connection to reversibility. They also offer approaches to study relations such as dependence, concurrency or causality between transitions, useful in exploring e.g., causes of bugs or how to multi-thread executions. This paper offers two main contributions: first, we provide separate definitions of a dependence relation and an independence relation, and prove their complementarity on connected transitions instead of postulating it, as is usually done. We also prove that those relations, as well as the notions of event, concurrency, causality and conflict, are unique for any reversible system respecting basic sanity axioms. Second, we prove that the operational definitions of core independence and causality coincide with their characterisations using a pre-existing syntactic mechanism in reversible process calculi, namely communication keys. 

   more » « less
2. Compositionality and Observational Refinement for Linearizability with Crashes

   https://doi.org/10.1145/3689792  

   Oliveira_Vale, Arthur; Wang, Zhongye; Chen, Yixuan; You, Peixin; Shao, Zhong (October 2024, Proceedings of the ACM on Programming Languages)

   Crash-safety is an important property of real systems, as the main functionality of some systems is resilience to crashes. Toward a compositional verification approach for crash-safety under full-system crashes, one observes that crashes propagate instantaneously to all components across all levels of abstraction, even to unspecified components, hindering compositionality. Furthermore, in the presence of concurrency, a correctness criterion that addresses both crashesandconcurrency proves necessary. For this, several adaptations of linearizability have been suggested, each featuring different trade-offs between complexity and expressiveness. The recently proposed compositional linearizability framework shows that to achieve compositionality with linearizability, both a locality and observational refinement property are necessary. Despite that, no linearizability criterion with crashes has been proven to support an observational refinement property. In this paper, we define a compositional model of concurrent computation with full-system crashes. We use this model to develop a compositional theory of linearizability with crashes, which reveals a criterion,crash-aware linearizability, as its inherent notion of linearizability and supports both locality and observational refinement. We then show that strict linearizability and durable linearizability factor through crash-aware linearizability as two different ways of translating between concurrent computation with and without crashes, enabling simple proofs of locality and observational refinement for a generalization of these two criteria. Then, we show how the theory can be connected with a program logic for durable and crash-aware linearizability, which gives the first program logic that verifies a form of linearizability with crashes. We showcase the advantages of compositionality by verifying a library facilitating programming persistent data structures and a fragment of a transactional interface for a file system. 

   more » « less
3. Alone together: compositional reasoning and inference for weak isolation

   https://doi.org/10.1145/3158115  

   Kaki, Gowtham; Nagar, Kartik; Najafzadeh, Mahsa; Jagannathan, Suresh (January 2018, Proceedings of the ACM on Programming Languages)

   Serializability is a well-understood correctness criterion that simplifies reasoning about the behavior of concurrent transactions by ensuring they are isolated from each other while they execute. However, enforcing serializable isolation comes at a steep cost in performance because it necessarily restricts opportunities to exploit concurrency even when such opportunities would not violate application-specific invariants. As a result, database systems in practice support, and often encourage, developers to implement transactions using weaker alternatives. These alternatives break the strong isolation guarantees offered by serializable transactions to permit greater concurrency. Unfortunately, the semantics of weak isolation is poorly understood, and usually explained only informally in terms of low-level implementation artifacts. Consequently, verifying high-level correctness properties in such environments remains a challenging problem. To address this issue, we present a novel program logic that enables compositional reasoning about the behavior of concurrently executing weakly-isolated transactions. Recognizing that the proof burden necessary to use this logic may dissuade application developers, we also describe an inference procedure based on this foundation that ascertains the weakest isolation level that still guarantees the safety of high-level consistency assertions associated with such transactions. The key to effective inference is the observation that weakly-isolated transactions can be viewed as functional (monadic) computations over an abstract database state, allowing us to treat their operations as state transformers over the database. This interpretation enables automated verification using off-the-shelf SMT solvers. Our development is parametric over a transaction’s specific isolation semantics, allowing it to be applicable over a range of concurrency control mechanisms. Case studies and experiments on real-world applications (written in an embedded DSL in OCaml) demonstrate the utility of our approach, and provide strong evidence that automated verification of weakly-isolated transactions can be placed on the same formal footing as their strongly-isolated serializable counterparts. 

   more » « less
4. Is This Correct? Let's Check!

   Ben-Eliezer, Omri; Mikulincer, Dan; Mossel, Elchanan; Sudan, Madhu (January 2023, 14th Innovations in Theoretical Computer Science Conference, {ITCS} 2023)

   Kaiai, Yael Tauman (Ed.)

   Societal accumulation of knowledge is a complex process. The correctness of new units of knowledge depends not only on the correctness of new reasoning, but also on the correctness of old units that the new one builds on. The errors in such accumulation processes are often remedied by error correction and detection heuristics. Motivating examples include the scientific process based on scientific publications, and software development based on libraries of code. Natural processes that aim to keep errors under control, such as peer review in scientific publications, and testing and debugging in software development, would typically check existing pieces of knowledge - both for the reasoning that generated them and the previous facts they rely on. In this work, we present a simple process that models such accumulation of knowledge and study the persistence (or lack thereof) of errors. We consider a simple probabilistic model for the generation of new units of knowledge based on the preferential attachment growth model, which additionally allows for errors. Furthermore, the process includes checks aimed at catching these errors. We investigate when effects of errors persist forever in the system (with positive probability) and when they get rooted out completely by the checking process. The two basic parameters associated with the checking process are the probability of conducting a check and the depth of the check. We show that errors are rooted out if checks are sufficiently frequent and sufficiently deep. In contrast, shallow or infrequent checks are insufficient to root out errors. 

   more » « less
5. Reversible to irreversible transitions in periodic driven many-body systems and future directions for classical and quantum systems

   https://doi.org/10.1103/PhysRevResearch.5.021001  

   Reichhardt, C; Regev, Ido; Dahmen, K; Okuma, S; Reichhardt, C_J O (May 2023, Physical Review Research)

   Reversible to irreversible (R-IR) transitions arise in numerous periodically driven collectively interacting systems that, after a certain number of driving cycles, organize into a reversible state where the particle trajectories repeat during every or every few cycles. On the irreversible side of the transition, the motion is chaotic. R-IR transitions were first systematically studied for periodically sheared dilute colloids, and have now been found in a wide variety of both soft and hard matter periodically driven systems, including amorphous solids, crystals, vortices in type-II superconductors, and magnetic textures. It has been shown that in several of these systems, the transition to a reversible state is an absorbing phase transition with a critical divergence in the organization timescale at the transition. The same systems are capable of storing multiple memories and may exhibit return point memory. We give an overview of R-IR transitions including recent advances in the field and discuss how the general framework of R-IR transitions could be applied to a much broader class of nonequilibrium systems in which periodic driving occurs, including not only soft and hard condensed matter systems, but also astrophysics, biological systems, and social systems. In particular, some likely candidate systems are commensurate-incommensurate states, systems exhibiting hysteresis or avalanches, nonequilibrium pattern forming states, and other systems with absorbing phase transitions. Periodic driving could be applied to hard condensed matter systems to see if organization into reversible states occurs for metal-insulator transitions, semiconductors, electron glasses, electron nematics, cold atom systems, or Bose-Einstein condensates. R-IR transitions could also be examined in dynamical systems where synchronization or phase locking occurs. We also discuss the possibility of using complex periodic driving, such as changing drive directions or using multiple frequencies, to determine whether these systems can still organize to reversible states or retain complex multiple memories. Finally, we describe features of classical and quantum time crystals that could suggest the occurrence of R-IR transitions in these systems. 

   more » « less