Compositional Development of Certified System Software

Explore the challenges and advancements in developing certified heterogeneous systems through this conference talk from ACM SIGPLAN's GALOP'24. Delve into the CertiKOS project's approach to specifying, programming, compiling, and composing large-scale certified systems. Learn how game semantics and algebraic effects are applied to support layered composition of deep specifications and certified abstraction layers. Discover a new general semantics for horizontal and vertical composition of linearizable concurrent objects. Examine the common issue of emergent behaviors in compositional models of concurrent computation and understand how category theory, specifically the Karoubi envelope, provides a solution. Gain insights into a novel formulation of linearizability that doesn't rely on atomicity or directly on happens-before ordering. Explore the intrinsic relationship between linearizability and compositionality, and how this new understanding impacts the theory and practice of building certified concurrent abstraction layers. This 49-minute talk by Zhong Shao offers a comprehensive overview of the latest developments in compositional development of certified system software.