Skip to content

Latest commit

 

History

History

mailbox

Folders and files

NameName
Last commit message
Last commit date

parent directory

..
README.txt
README.txt
 
 
atomic_exchange.c
atomic_exchange.c
 
 
atomic_exchange.h
atomic_exchange.h
 
 
atomic_exchange.v
atomic_exchange.v
 
 
faster_lockfree_linsearch.c
faster_lockfree_linsearch.c
 
 
faster_lockfree_linsearch.v
faster_lockfree_linsearch.v
 
 
lock.c
lock.c
 
 
lock.v
lock.v
 
 
lockfree_linsearch.c
lockfree_linsearch.c
 
 
lockfree_linsearch.v
lockfree_linsearch.v
 
 
mailbox.c
mailbox.c
 
 
mailbox.v
mailbox.v
 
 
mailbox1.c
mailbox1.c
 
 
mailbox_bad.c
mailbox_bad.c
 
 
mailbox_bad.v
mailbox_bad.v
 
 
oplistset.c
oplistset.c
 
 
oplistset.v
oplistset.v
 
 
stdlib.h
stdlib.h
 
 
threads.c
threads.c
 
 
threads.h
threads.h
 
 
verif_atomic_exchange.v
verif_atomic_exchange.v
 
 
verif_lock.v
verif_lock.v
 
 
verif_lockfree_linsearch.v
verif_lockfree_linsearch.v
 
 
verif_mailbox_all.v
verif_mailbox_all.v
 
 
verif_mailbox_bad_main.v
verif_mailbox_bad_main.v
 
 
verif_mailbox_bad_read.v
verif_mailbox_bad_read.v
 
 
verif_mailbox_bad_specs.v
verif_mailbox_bad_specs.v
 
 
verif_mailbox_bad_write.v
verif_mailbox_bad_write.v
 
 
verif_mailbox_init.v
verif_mailbox_init.v
 
 
verif_mailbox_main.v
verif_mailbox_main.v
 
 
verif_mailbox_read.v
verif_mailbox_read.v
 
 
verif_mailbox_reader.v
verif_mailbox_reader.v
 
 
verif_mailbox_specs.v
verif_mailbox_specs.v
 
 
verif_mailbox_write.v
verif_mailbox_write.v
 
 
verif_mailbox_writer.v
verif_mailbox_writer.v
 
 
verif_oplistset.v
verif_oplistset.v
 
 

README.txt

The extension of VST with SC and RA atomics consists of:
general_atomics.v - invariants, SC atomics, and logical atomicity (Section 4.2 of the POPL submission)
acq_rel_atomics.v, acq_rel_SW.v - axiomatic specifications of release-acquire atomics (Section 4.3)
gen_atomics.h, gen_atomics.h - C interface for our atomics
The following files for each concurrent data structure <D> in {kvnode_atomic (6.2.1), hashtable_atomic (6.2.2), kvnode_atomic_ra (6.3.1), hashtable_atomic_ra (6.3.2)}:
<D>.c - C code for the data structure
<D>.v - Coq representation of the C code generated via CompCert clightgen
verif_<D>.v - specifications and proofs of correctness for the data structure