README.txt 3.63 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19

DESCRIPTION

  This folder contains the Coq development for
  Iris: Monoids and Invariants as an Orthogonal Basis for Concurrent Reasoning

  by
  
  Ralf Jung <jung@mpi-sws.org>
  David Swasey <swasey@mpi-sws.org>
  Filip Sieczkowski <filips@cs.au.dk>
  Kasper Svendsen <ksvendsen@cs.au.dk>
  Aaron Turon <turon@mpi-sws.org>
  Lars Birkedal <birkedal@cs.au.dk>
  Derek Dreyer <dreyer@mpi-sws.org>


CONTENTS

Derek Dreyer's avatar
Derek Dreyer committed
20 21
  Our artifact is a Coq formalization of the model of our Iris logic,
  together with a proof of adequacy (establishing that the model is
22
  faithful wrt the operational semantics) and a proof of soundness of
Derek Dreyer's avatar
Derek Dreyer committed
23 24
  the primitive rules of the logic wrt the model.

25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45
  NOTE: We have just mechanized the *soundness* of the *primitive*
  rules of Iris in Coq.  We have not mechanized the proofs of derived
  rules (i.e. those derivable from the primitive rules), nor have we
  mechanized the case study or other examples that are proven within
  the logic.  Proof outlines for the latter are given in the appendix
  that accompanied the POPL submission, and will be fleshed out even
  further for the final version of the appendix.

  The reason we focused on the primitive rules is that those are the
  rules whose soundness is proven by direct appeal to the semantic
  model of Iris.  For space reasons, we did not want to present the
  semantic model of Iris in any detail in the paper, but we still
  wanted to give the reader confidence in the results of the paper.
  With our Coq mechanization in hand, the reader can safely ignore the
  semantic model and instead focus on how to *use* the primitive rules
  of the logic (to derive more sophisticated rules or prove
  interesting examples).

  Mechanizing Iris proofs is a very interesting and important
  direction for future work, but it is beyond the scope of the paper.

Derek Dreyer's avatar
Derek Dreyer committed
46

47
  The folder is organized as follows:
Derek Dreyer's avatar
Derek Dreyer committed
48

49
  * core_lang.v contains the axioms about the language
Derek Dreyer's avatar
Derek Dreyer committed
50 51 52 53

  * lang.v defines the threadpool reduction and derives some lemmas
    from core_lang.v
  
54
  * masks.v introduces some lemmas about masks
Derek Dreyer's avatar
Derek Dreyer committed
55
  
56 57
  * world_prop.v uses the ModuRes Coq library to construct the domain
    for Iris propositions
Derek Dreyer's avatar
Derek Dreyer committed
58
  
David Swasey's avatar
David Swasey committed
59
  * iris_core.v defines world satisfaction and the simpler assertions
60
  
61 62
  * iris_vs.v defines view shifts and proves their rules
  
63 64
  * iris_wp.v defines weakest preconditions and proves the rules for
    Hoare triples
David Swasey's avatar
David Swasey committed
65 66
  
  * iris_unsafe.v proves rules for unsafe Hoare triples
67

Filip Sieczkowski's avatar
Filip Sieczkowski committed
68 69 70 71
  The development uses ModuRes, a Coq library by Sieczkowski et al. to
  solve the recursive domain equation (see the paper for a reference)
  and prove some of the standard separation logic rules. It is located
  in the lib/ subdirectory.
72 73 74 75 76 77


REQUIREMENTS

  Coq 

78 79
  We have tested the development using Coq 8.4pl4 on Linux and Mac
  machines. The entire compilation took less than an hour.
80 81 82 83 84 85
  

HOW TO COMPILE

  To compile the development, run
  
86
  > (cd lib/ModuRes; make) && make 
87 88

  in the folder containing this README. 
Derek Dreyer's avatar
Derek Dreyer committed
89
  
90 91 92 93


OVERVIEW OF LEMMAS

94
  Below we give a mapping from proof rules in the paper to Coq lemma's.
95 96 97

  RULE         Coq lemma
  -----------------------
98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115
  VSTimeless   iris_vs.v:/vsTimeless
  NewInv       iris_vs.v:/vsNewInv
  InvOpen      iris_vs.v:/vsOpen
  InvClose     iris_vs.v:/vsClose
  VSTrans      iris_vs.v:/vsTrans
  VSImp        iris_vs.v:/vsEnt
  VSFrame      iris_vs.v:/vsFrame
  FpUpd        iris_vs.v:/vsGhostUpd

  Ret          iris_wp.v:/htRet
  Bind         iris_wp.v:/htBind
  Frame        iris_wp.v:/htFrame
  AFrame       iris_wp.v:/htAFrame
  Csq          iris_wp.v:/htCons
  ACSQ         iris_wp.v:/htACons
  Fork         iris_wp.v:/htFork

  The main adequacy result is expressed by Theorem
116
  iris_wp.v:/adequacy_obs.
117