Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Realizability in Semantics-Guided Synthesis Done Eagerly

Roland Meyer, Jakob Tepe, Sebastian Wolff

TL;DR

This work presents realizability and realization logic, two program logics that jointly address the problem of finding solutions in semantics-guided synthesis and shows how to implement the program logics using verification conditions, and reports on experiments with a prototype in the context of safe memory reclamation for lock-free data structures.

Abstract

We present realizability and realization logic, two program logics that jointly address the problem of finding solutions in semantics-guided synthesis. What is new is that we proceed eagerly and not only analyze a single candidate program but a whole set. Realizability logic computes information about the set of candidate programs in a forward fashion. Realization logic uses this information as guidance to identify a suitable candidate in a backward fashion. Realizability logic is able to analyze a set of programs due to a new form of assertions that tracks synthesis alternatives. Realizability logic then picks alternatives to arrive at a program, and we give the guarantee that this process will not need backtracking. We show how to implement the program logics using verification conditions, and report on experiments with a prototype in the context of safe memory reclamation for lock-free data structures.

Realizability in Semantics-Guided Synthesis Done Eagerly

TL;DR

This work presents realizability and realization logic, two program logics that jointly address the problem of finding solutions in semantics-guided synthesis and shows how to implement the program logics using verification conditions, and reports on experiments with a prototype in the context of safe memory reclamation for lock-free data structures.

Abstract

We present realizability and realization logic, two program logics that jointly address the problem of finding solutions in semantics-guided synthesis. What is new is that we proceed eagerly and not only analyze a single candidate program but a whole set. Realizability logic computes information about the set of candidate programs in a forward fashion. Realization logic uses this information as guidance to identify a suitable candidate in a backward fashion. Realizability logic is able to analyze a set of programs due to a new form of assertions that tracks synthesis alternatives. Realizability logic then picks alternatives to arrive at a program, and we give the guarantee that this process will not need backtracking. We show how to implement the program logics using verification conditions, and report on experiments with a prototype in the context of safe memory reclamation for lock-free data structures.
Paper Structure (34 sections, 37 theorems, 139 equations, 16 figures, 1 table)

This paper contains 34 sections, 37 theorems, 139 equations, 16 figures, 1 table.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Parameters
  4. Programs
  5. Hoare Logic
  6. Realizability Logic
  7. Sketches
  8. Realizability Logic
  9. Discussion
  10. Realization Logic
  11. Implementing Realizability Logic
  12. Verification Conditions and Strongest Post
  13. Example: Checking Realizability of the Factorial Function
  14. Implementing Realization Logic
  15. Example: Synthesizing Factorial Function
  16. ...and 19 more sections

Key Result

theorem 1

$\vdash_{a} \boldsymbol{\langle}\mathit{R}\boldsymbol{\rangle} \texttt{sketch} \boldsymbol{\langle}\mathit{S}\boldsymbol{\rangle}$ if and only if $\models_{a} \boldsymbol{\langle}\mathit{R}\boldsymbol{\rangle} \texttt{sketch} \boldsymbol{\langle}\mathit{S}\boldsymbol{\rangle}$ .

Figures (16)

  • Figure 1: Proof outline in realizability logic.
  • Figure 2: Proof outline derived from \ref{['code:introa']}.
  • Figure 3: Rules of realizability logic. Extensions of Hoare logic are highlighted in blue.
  • Figure 4: Demonic choice.
  • Figure 5: Subproof sharing.
  • ...and 11 more figures

Theorems & Definitions (78)

  • theorem 1: Sound-And-Complete
  • proof
  • theorem 2: Soundness
  • lemma 1
  • theorem 3: Completeness
  • theorem 4: Backtracking Freedom
  • theorem 5: VC-Sound-And-Complete
  • theorem 6: SP-Sound-And-Complete
  • theorem 7: $\mathit{syn}$-Sound-And-Complete
  • lemma 2
  • ...and 68 more