Skip to content

Proofs for the paper "Risotto: A Dynamic Binary Translator for Weak Memory Model Architectures"

Notifications You must be signed in to change notification settings

binary-translation/risotto-proofs

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 

History

5 Commits
 
 
 
 
 
 
 
 
 
 
 
 
 
 

Repository files navigation

Risotto: Architecture Mapping Proofs

Proofs for translating memory instructions between different CPU architectures, written in Agda. For the paper "Risotto: A Dynamic Binary Translator for Weak Memory Model Architectures"

Running/Checking

  • Install Agda (v.2.6.2) with its standard library
  • Make sure Agda can find the standard library (see the ~/.agda/libraries and ~/.agda/defaults files in the installation instructions)

⚠️ The proofs were developed with standard library version 1.7.1. Other versions may be incompatible.

There are multiple ways of type-checking the proofs; Two are listed below.

Running/Checking: Command Line

The easiest way of checking the proofs is through a terminal.

  • Run agda src/Main.agda --safe.

Once a proof type-checks, it's correct. Also check the "Code Navigation" section below to understand what it is proving.

Running/Checking: Emacs

Another way of checking the proofs is with the agda-mode in Emacs.

  • Install Emacs
  • Install agda-mode as described in Agda's install instructions (above).
  • Load an .agda file in Emacs, and press C-c C-l to type-check the file.

If a proof type-checks, it's correct. Also check the "Code Navigation" section below to understand what it is proving.

Code Navigation

The proofs consists of several parts (in src/):

  • Main.agda - Links to all proofs
  • Arch/ - Memory model specifications for architectures
    • General/ - A general specification of an execution in the axiomatic model. This is instantiated by the individual architectures (below).
    • Armv8.agda - The "Armed Cats" Armv8 model, with our proposed change
    • X86.agda - The X86 model
    • TCG.agda - Our TCG model
  • Map*to*.agda - The specification of mapping executions between architectures
  • Transform*.agda - The specificaton of elimination and reordering transformations on TCG
  • Proof/ - Contains all the proofs (also referenced by Main.agda)
    • Framework.agda - A general framework for memory model proofs
    • Mapping/ - The mapping proofs between architectures
      • Framework.agda - A framework for architecture-mapping proofs. Extends the general framework
    • Elimination/ - Elimination proofs
    • Reorder/ - Reordering proofs

About

Proofs for the paper "Risotto: A Dynamic Binary Translator for Weak Memory Model Architectures"

Topics

Resources

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published

Languages