Omnisemantics: Smooth Handling of Nondeterminism - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Article Dans Une Revue ACM Transactions on Programming Languages and Systems (TOPLAS) Année : 2023

Omnisemantics: Smooth Handling of Nondeterminism

Résumé

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.
Fichier principal
Vignette du fichier
omnisemantics.pdf (795.38 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)

Dates et versions

hal-03255472 , version 1 (09-06-2021)
hal-03255472 , version 2 (17-03-2022)
hal-03255472 , version 3 (28-09-2022)

Licence

Paternité

Identifiants

Citer

Arthur Charguéraud, Adam Chlipala, Andres Erbsen, Samuel Gruetter. Omnisemantics: Smooth Handling of Nondeterminism. ACM Transactions on Programming Languages and Systems (TOPLAS), 2023, 45 (1), pp.1-43. ⟨10.1145/3579834⟩. ⟨hal-03255472v3⟩
521 Consultations
397 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More