===============================================================================
|                                                                             |
|Certifying Low-Level Programs with Hardware Interrupts and Preemptive Threads|
|                                                                             |
| * Xinyu Feng, Zhong Shao, Yuan Dong and Yu Guo                              |
|                                                                             |
| * Published In Proc. 2008 ACM SIGPLAN Conference on Programming Language    |
|   Design and Implementation (PLDI'08), Tucson, Arizona, pages to appear.    |
===============================================================================

* Coq implementation code (Coq v8.1-pl3)

  ** Authors : Xinyu Feng, Zhong Shao, Yuan Dong, Yu Guo
	       Wei Wang, Haibo Wang and Xi Wang

  ** Download : http://flint.cs.yale.edu/publications/aim.html

* Files

./  
  Coqlib.v                      Base definitions
  Arith_Lemmas.v                Lemmas for arithmetic
  ListT.v                       List in Type universe
  Map.v                         Map structure
  MultiMapT.v                   Multiple map structure
  Assertion.v                   Assertion language definitions
  Reg.v                         Registers file definition
  Machine.v                     Machine definition
  Operational_Semantics.v       Operational semantics
  Mem_Lemmas.v                  Lemmas for memory
  OpSem_Lemmas.v                Lemmas for operational semantics
  OpSem_Lemmas2.v               Lemmas for operational semantics
  Assertion_Lemmas.v            Lemmas for assertions
  Assertion_Lemmas2.v           Lemmas for assertions
  Assertion_Lemmas3.v           Lemmas for assertions
  Assertion_Lemmas4.v           Lemmas for assertions
  Assertion_Lemmas5.v           Lemmas for assertions

./CAP0
  CAP0.v                        CAP0 (OCAP) definition
  Soundness.v                   Soundness proof of CAP0
  Link.v                        Link definition and lemmas

./SCAP
  AIM.v                         AIM base definitions 
  AIM_Lemmas.v                  Lemmas for AIM
  QLib.v                        Double linked queue definition
  QLemmas.v                     Lemmas for queue
  SCAP.v                        SCAP logic for kernel primitives
  SCAP_Itr.v                    SCAP logic for interrupt handlers
  SCAP_READY.v                  SCAP logic for user threads
  SCAP_IDLE.v                   SCAP logic for idle thread
  Linking.v                     Linking (4 logics) together
  Linking_Lemmas.v              Lemmas for AIM logic
  Linking_Lemmas2.v             Lemmas for AIM logic
  Linking_Lemmas3.v             Lemmas for AIM logic
  READY_SW.v                    Lemmas for soundness proof
  NH_SW.v                       Lemmas for soundness proof
  IH_SW.v                       Lemmas for soundness proof
  READY_BLK.v                   Lemmas for soundness proof
  READY_UNBLK.v                 Lemmas for soundness proof
  SCAP_Soundness.v              Soundness proof of SCAP
  SCAP_Itr_Lemmas.v             Lemmas for SCAP_Itr soundness
  SCAP_Itr_Soundness.v          Soundness proof of SCAP_Itr
  SCAP_NH_Lemmas.v              Lemmas for soudness proof
  SCAP_READY_Soundness.v        Soundness proof of SCAP_READY
  SCAP_IDLE_Soundness.v         Soundness proof of SCAP_IDLE

./miniOS
  Kernel.v                      Assembly code of kernel
  EnQueueSpec.v                 enQueue specification
  EnQueueProof.v                enQueue proof
  DeQueueSpec.v                 deQueue specification
  DeQueueProof.v                deQueue proof
  SwitchSpec.v                  scheduler specification
  SwitchProof.v                 scheduler proof
  BlockSpec.v                   block specification
  BlockProof.v                  block proof
  UnblockSpec.v                 unblock specification
  UnblockProof.v                unblock proof
  SleepSpec.v                   sleep specification
  SleepProof.v                  sleep proof
  Timer.v                       timer specification
  TimerProof.v                  timer proof
  YieldSpec.v                   yield specification
  YieldProof.v                  yield proof

./examples
  Assembly.v                    Assembly code of examples
  SyncUtil.v                    Lemmas
  cond_signal.v                 signal specification % proof
  cond_wait.v                   wait specification % proof
  lock_acquire.v                lock_acquire specification % proof
  lock_release.v                lock_release specification % proof

* Compiling
  
  ** tar -zxf aim-code.tar.gz
  ** cd aim-code; make all

* Statistic 
 
  ** Total lines of code : 76747
  ** Total number of definitions : 1176
  ** Total number of lemmas/theorems : 1847
