From d26d0c7f3607bc7c07ec2dc3e41e4cb6a0d42f81 Mon Sep 17 00:00:00 2001
From: Kasper Svendsen
Date: Sun, 5 Oct 2014 21:59:44 +0200
Subject: [PATCH] Updated the README file slightly.

README.txt  94 ++++++++++++++++++++++++++++++++++++++++
1 file changed, 70 insertions(+), 24 deletions()
diff git a/README.txt b/README.txt
index c2710004..441e2baa 100644
 a/README.txt
+++ b/README.txt
@@ 1,24 +1,70 @@
This folder contains the Coq development for
Iris: Monoids and Invariants as an Orthogonal Basis for Concurrent Reasoning
by
Ralf Jung
David Swasey
Filip Sieczkowski
Kasper Svendsen
Aaron Turon
Lars Birkedal
Derek Dreyer


It uses a Coq library in lib/ by Sieczkowski et al. to solve the recursive domain equation (see the paper for a reference).

This folder is organized as follows:
* core_lang.v contains the axioms about the language
* lang.v defines the threadpool reduction and derives some lemmas from core_lang.v
* masks.v introduces some lemmas about masks
* world_prop.v uses the aforementioned Coq library to construct the domain for Iris propositions
* iris.v is the main file and contains the actual logic and the proof of the rules for view shifts and Hoare tiples

Run "make" in this folder to build it all.
Be aware that iris.v takes a long time to check and needs significant amounts of RAM!
8GiB may be sufficient, but to be safe you should have 16GiB and give it around 2 to 3 hours.
+
+DESCRIPTION
+
+ This folder contains the Coq development for
+ Iris: Monoids and Invariants as an Orthogonal Basis for Concurrent Reasoning
+
+ by
+
+ Ralf Jung
+ David Swasey
+ Filip Sieczkowski
+ Kasper Svendsen
+ Aaron Turon
+ Lars Birkedal
+ Derek Dreyer
+
+
+CONTENTS
+
+ The folder is organized as follows:
+ * core_lang.v contains the axioms about the language
+ * lang.v defines the threadpool reduction and derives some lemmas from core_lang.v
+ * masks.v introduces some lemmas about masks
+ * world_prop.v uses the aforementioned Coq library to construct the domain for Iris propositions
+ * iris.v is the main file and contains the actual logic and the proof of the rules for view shifts and Hoare tiples
+
+ It uses a Coq library in lib/ by Sieczkowski et al. to solve the recursive domain equation (see the paper for a reference).
+
+
+REQUIREMENTS
+
+ Coq
+ 8GB ram
+
+ We have tested the development using Coq v. 8.4pl4 on a machine with 8GB RAM + 4GB swap.
+
+
+HOW TO COMPILE
+
+ To compile the development, run
+
+ > make
+
+ in the folder containing this README.
+
+ Be aware that iris.v takes a long time to check and needs significant amounts of RAM!
+ 8GiB may be sufficient, but to be safe you should have 16GiB and give it around 2 to 3 hours.
+
+
+OVERVIEW OF LEMMAS
+
+ Below we give a mapping from proof rules in the paper to Coq lemma's in Iris.v
+
+ RULE Coq lemma
+ 
+ VSTimeless vsTimeless
+ NewInv vsNewInv
+ VSOpen vsOpen
+ VSClose vsClose
+ VSTrans vsTrans
+ VSImp vsEnt
+ GhostUpd vsGhostUpd
+
+ Ret htRet
+ Bind htBind
+ Frame htFrame
+ Csq htCons
+ ACSQ htACons
+
+ The main adequacy result is expressed by Theorem soundness_obs.

2.26.2