Skip to Main content Skip to Navigation
New interface
Preprints, Working Papers, ...

Omnisemantics: Smooth Handling of Nondeterminism

Arthur Charguéraud 1 Adam Chlipala 2 Andres Erbsen 2 Samuel Gruetter 2 
1 CAMUS - Compilation pour les Architectures MUlti-coeurS
Inria Nancy - Grand Est, ICube - Laboratoire des sciences de l'ingénieur, de l'informatique et de l'imagerie
Abstract : This paper gives an in-depth presentation of the omni-big-step and omni-small-step styles of semantic judgments. These styles describe operational semantics by relating starting states to sets of outcomes rather than to individual outcomes. A single derivation of these semantics for a particular starting state and program describes all possible nondeterministic executions (hence the name "omni"), whereas in traditional small-step and big-step semantics, each derivation only talks about one single execution. This restructuring allows for straightforward modeling of languages featuring both nondeterminism and undefined behavior. Specifically, omnisemantics inherently assert safety, i.e. they guarantee that none of the execution branches gets stuck, while traditional semantics need either a separate judgment or additional error markers to specify safety in the presence of nondeterminism. Omnisemantics can be understood as an inductively defined weakest-precondition semantics (or more generally, predicate-transformer semantics) that does not involve invariants for loops and recursion, but instead uses unrolling rules like in traditional small-step and big-step semantics. Omnisemantics have already been used in the past, but we believe that it has been under-appreciated and that it deserves a well-motivated, extensive and pedagogical presentation of its benefits. We also explore several novel aspects associated with these semantics, in particular their use in type-soundness proofs for lambda calculi, partial-correctness reasoning, and forward proofs of compiler correctness for terminating but potentially nondeterministic programs being compiled to nondeterministic target languages. All results in this paper are formalized in Coq.
Document type :
Preprints, Working Papers, ...
Complete list of metadata

https://hal.inria.fr/hal-03255472
Contributor : Arthur Charguéraud Connect in order to contact the contributor
Submitted on : Wednesday, September 28, 2022 - 11:19:16 AM
Last modification on : Friday, November 18, 2022 - 9:27:15 AM

File

omnisemantics.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-03255472, version 3

Citation

Arthur Charguéraud, Adam Chlipala, Andres Erbsen, Samuel Gruetter. Omnisemantics: Smooth Handling of Nondeterminism. {date}. ⟨hal-03255472v3⟩

Share

Metrics

Record views

195

Files downloads

283