Fine-grained Concurrent Separation Logic
========================================

Supplementary material for the paper entitled

"Mechanized Verification of Fine-grained Concurrent Programs",
submitted for publication at PLDI 2015

This directory contains all main development focusing on FCSL and
its deviations for reasoning about different fine-grained data
structures. This project builds on several important components:

  * Hoare Type Theory for reasoning about imperative programs
  * Implementation of semantics for concurrency
  * Coq/SSReflect libraries

Building and executing artifacts
================================

*** REQUIREMENTS ***

Coq 8.4       (https://coq.inria.fr/download)
SSReflect 1.4 (http://ssr.msr-inria.inria.fr/)

(For SSReflect 1.5, you will need to install the "Mathematical
Components" libraries. The current FCSL implementation wasn't
tested with them).

After installing SSReflect, make sure to have the following
environment variables properly declared.

*** ENVIRONMENT VARIABLES ***

COQC=[...]/ssreflect-1.4/bin/ssrcoq
COQBIN=[...]/coq-8.4/bin/
COQ_MK=[...]/coq-8.4/bin/coq_makefile
SSRCOQ_LIB=[...]/ssreflect-1.4/theories

COQBIN and COQ_MK can be empty if they are in the PATH.

*** BUILD ***

make clean; make

*** Counting lines of code ***

For counting lines in an individual file (e.g., spanning.v), run

./count spanning.v

Structure of the repository
===========================

File                   Description
-------------------    ----------------------------------------------------

README                 This file

Makefile               Build file

Makefile.BUILD         Additional build scripts

cloc                   An utility to count lines of code
		       (see http://cloc.sourceforge.net/)

count                  A script running 'cloc'

---------------------------------------------------------------------------
                      Metatheory of FCSL
---------------------------------------------------------------------------

idynamic.v             Support for dynamic typing in heaps

pcm.v                  Implementation of partial commutative monoids (PCMs)

unionmap.v             Reference implementation of finite maps  	       

heap.v                 Refined implementation of heaps

codes.v                Enumeration of frequently used PCMs and types. Needed to make
                       checking of equality on pcm and type *codes* decidable.

feaps.v                PCM of heap maps

state.v                states as triples of maps

zigzag.v               Definition and helper lemmas about <\ and /> operators
                       used in the fork-join closure

worlds.v               Definition of concurroids, with properties on states and
                       transitions

auto_split.v           Some automation using overloaded lemmas

inject.v               Meta theory required for proving the injection rule
                       
atomic.v               Definition and properties of atomic actions

rely.v                 Definition of the rely predicate for a concurroid

privstate.v            Concurroid for thread-local state

footprint.v            Helper lemmas about disjointness of labels

retract.v              Meta theory required for proving the hiding rule

schedule.v             Data type of paths

process.v              Definition of action trees

always.v               Definition of the modal predicates for adherence to a
                       protocol

model.v                Implementation of denotational semantics of programs as sets
                       of trees

lemmas.v               Soundness of the rules; essentially each lemma is a case 
                       in the proof of the Soundness theorem. 

histories.v            A library for history PCMs used in specifications of
                       optimistic fine-grained algorithms

stsep.v                Notation for traditional-style unary Hoare pre/postconditions

---------------------------------------------------------------------------
                           Example programs
---------------------------------------------------------------------------

locks.v                A generic interface for locks 

caslock.v              An implementation of a CAS-based spin lock concurroid, its
		       actions, lock/unlock procedures and lemmas for Hoare-style reasoning

ticketed.v             An implementation of a ticketed lock concurroid, its
		       actions, lock/unlock procedures and lemmas for Hoare-style reasoning

incrementor.v          A toy example of a coarse-grained incrementor.

alloc.v                A simple coarse-grained memory allocator

readpair.v             An implementation of an atomic pair-snapshot data structure

treiber.v              An implementation of Treiber's non-blocking stack

stack_framed.v         A demonstation of a frame rule applied to the Stack 
		       specifications

stack_seq.v            A derivation of a sequential specification for
		       the Treiber stack "push" and "pop" operations

stack_client.v         A simple stack client - two-thread producer/consumer

flatcombine.v          A generic implementation of the Flat Combiner, parametrized
		       by specifications of sequential procedures

stack_combine.v	       Instantiation of the Flat Combiner with Treiber-style sequential 
		       stack push/pop procedures

spanning.v             A concurrent version of a DFS-style in-place computation of 
		       a graph spanning tree (full functional correctness verified).

---------------------------------------------------------------------------
              Hoare Type Theory-specific files
    (not interesting, but necessary for FCSL development)
---------------------------------------------------------------------------

pred.v                 Basic propositional equalities

prelude.v              Basic definitions of setoid equalities

ordtype.v              Implementation of ordered types

finmap.v 	       Theory of finite maps

pperm.v 	       A theory of permutations over non-equality types

domain.v 	       Implementation of partially-ordered sets

array.v                A simple theory of arrays based on finite maps
