An official website of the United States government
Large-scale software verification relies critically on the use of compositional languages, semantic models, specifications, and verification techniques. Recent work on certified abstraction layers synthesizes game semantics, the refinement calculus, and algebraic effects to enable the composition of heterogeneous components into larger certified systems. However, in existing models of certified abstraction layers, compositionality is restricted by the lack of encapsulation of state. In this paper, we present a novel game model for certified abstraction layers where the semantics of layer interfaces and implementations are defined solely based on their observable behaviors. Our key idea is to leverage Reddy's pioneer work on modeling the semantics of imperative languages not as functions on global states but as objects with their observable behaviors. We show that a layer interface can be modeled as an object type (i.e., a layer signature) plus an object strategy. A layer implementation is then essentially a regular map, in the sense of Reddy, from an object with the underlay signature to that with the overlay signature. A layer implementation is certified when its composition with the underlay object strategy implements the overlay object strategy. We also describe an extension that allows for non-determinism in layer interfaces. After formulating layer implementations as regular maps between object spaces, we move to concurrency and design a notion of concurrent object space, where sequential traces may be identified modulo permutation of independent operations. We show how to express protected shared object concurrency, and a ticket lock implementation, in a simple model based on regular maps between concurrent object spaces.
more »
« less
Refinement-Based Game Semantics and Certified Abstraction Layers
Formal methods have advanced to the point where the functional correctness of various large system components has been mechanically verified. However, the diversity of semantic models used across projects makes it difficult to connect these component to build larger certified systems. Given this, we seek to embed these models and proofs into a general-purpose framework where they could interact. We believe that a synthesis of game semantics, the refinement calculus, and algebraic effects can provide such a framework. To combine game semantics and refinement, we replace the downset completion typically used to construct strategies from posets of plays. Using the free completely distributive completion, we construct strategy specifications equipped with arbitrary angelic and demonic choices and ordered by a generalization of alternating refinement. This provides a novel approach to nondeterminism in game semantics. Connecting algebraic effects and game semantics, we interpret effect signatures as games and define two categories of effect signatures and strategy specifications. The resulting models are sufficient to represent the behaviors of a variety of low-level components, including the certified abstraction layers used to verify the operating system kernel CertiKOS.
more »
« less
- PAR ID:
- 10149882
- Date Published:
- Journal Name:
- Proc. 35th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS'20)
- Format(s):
- Medium: X
- Sponsoring Org:
- National Science Foundation
More Like this
-
-
Since the introduction of CompCert, researchers have been refining its language semantics and correctness theorem, and used them as components in software verification efforts. Meanwhile, artifacts ranging from CPU designs to network protocols have been successfully verified, and there is interest in making them interoperable to tackle end-to-end verification at an even larger scale. Recent work shows that a synthesis of game semantics, refinement-based methods, and abstraction layers has the potential to serve as a common theory of certified components. Integrating certified compilers to such a theory is a critical goal. However, none of the existing variants of CompCert meets the requirements we have identified for this task. CompCertO extends the correctness theorem of CompCert to characterize compiled program components directly in terms of their interaction with each other. Through a careful and compositional treatment of calling conventions, this is achieved with minimal effort.more » « less
-
Effect systems are lightweight extensions to type systems that can verify a wide range of important properties with modest developer burden. But our general understanding of effect systems is limited primarily to systems where the order of effects is irrelevant. Understanding such systems in terms of a semilattice of effects grounds understanding of the essential issues and provides guidance when designing new effect systems. By contrast, sequential effect systems—where the order of effects is important—lack an established algebraic structure on effects. We present an abstract polymorphic effect system parameterized by an effect quantale—an algebraic structure with well-defined properties that can model the effects of a range of existing sequential effect systems. We define effect quantales, derive useful properties, and show how they cleanly model a variety of known sequential effect systems. We show that for most effect quantales, there is an induced notion of iterating a sequential effect; that for systems we consider the derived iteration agrees with the manually designed iteration operators in prior work; and that this induced notion of iteration is as precise as possible when defined. We also position effect quantales with respect to work on categorical semantics for sequential effect systems, clarifying the distinctions between these systems and our own in the course of giving a thorough survey of these frameworks. Our derived iteration construct should generalize to these semantic structures, addressing limitations of that work. Finally, we consider the relationship between sequential effects and Kleene Algebras, where the latter may be used as instances of the former.more » « less
-
Formal verification is a gold standard for building reliable computer systems. Certified systems in particular come with a formal specification, and a proof of correctness which can easily be checked by a third party. Unfortunately, verifying large-scale, heterogeneous systems remains out of reach of current techniques. Addressing this challenge will require the use of compositional methods capable of accommodating and interfacing a range of program verification and certified compilation techniques. In principle, compositional semantics could play a role in enabling this kind of flexibility, but in practice existing tools tend to rely on simple and specialized operational models which are difficult to interface with one another. To tackle this issue, we present a compositional semantics framework which can accommodate a broad range of verification techniques. Its core is a three-dimensional algebra of refinement which operates across program modules, levels of abstraction, and components of the system's state. Our framework is mechanized in the Coq proof assistant and we showcase its capabilities with multiple use cases.more » « less
-
This study examined the relations among strategic planning, execution, and strategy efficiency during problem-solving in a digital algebra learning game with 7th-grade students. We used pre-solving pause time as a proxy indicator of strategic planning, and the productivity of the initial strategy as a measure of effective strategy execution. Additionally, we explored how these variables correlated with students’ posttest scores assessing algebraic knowledge. Mediation analyses at both the problem and student levels indicated that longer pre-solving pause times were associated with greater strategy efficiency. When considering both the direct and indirect effects of pre-solving pause time on strategy efficiency, the results revealed a partial positive mediation through the productivity of the initial strategy. Lastly, the results of a path analysis showed that strategy efficiency significantly predicted algebraic knowledge with a positive effect. These findings suggest that longer pause times are associated with more efficient problem solving as they increase the likelihood of a productive initial step, highlighting a positive mediating role of execution in the relation between planning and strategy efficiency in algebraic problem solving.more » « less
- Free Publicly Accessible Full Text
-
Accepted Manuscript1.0
- Conference Paper:
- The DOI is not currently available.
