Experimental Artifacts

This webpage describes the experimental artificats for the case studies in the dissertation.
  1. Superword level parallelism compiler transformation (http://ccs.neu.edu/home/jmitesh/dissertation/scalar-vector)

    A directory containing ACL2s model of the scalar and vector machine for superword level parallelism transformation.

    It also contains the proof script for correctness of the transformation based on SKS. Details of installing ACL2s and certifying are in the README file in the directory.

  2. Stack Machine (http://ccs.neu.edu/home/jmitesh/dissertation/stack-machine)

    This directory contains AIGs used for the comparing running time of model-checkers of IO equivalence and SKS for a JVM-inspired stack machines (STK and BSTK). The operational semantics of the machines are described in the paper.

    It also contains an executable to generate models for stack machines and correctness condition based on IO equivalence and SKS. More details on the usage are provided in the README file in the directory.

  3. Memory Controller (http://ccs.neu.edu/home/jmitesh/dissertation/memory-controller)

    This directory contains AIGs used for the comparing running time of model-checkers of IO equivalence and SKS for optimized memory controller. The operational semantics of the machines are described in the paper.

    It also contains an executable to generate models for memory controller and correctness condition based on IO equivalence and SKS. More details on the usage are provided in the README file in the directory.

  4. Event Processing System (http://www.ccs.neu.edu/home/jmitesh/dissertation/eps ) This directory contains the ACL2s model of AEPS, the abstract event processing system, PEPS, the optimized event processing system, and ACL2s proof script. The (eps-semantics.lisp ) contains the definitions formalizing the model and the top-level theorems to prove that PEPS is a skipping refinement of AEPS. The actual proof are in (eps-thms.lisp ).

    5. Model-checkers used in the experiments

    1. blimc (ats1 version)
      run command: ./blimc <bound> <aig-name>
      where bound = number of instructions + 2 (in case of stack machine) and
      = number of requests + 2 (in case of memory controller)

    2. IIMC (version 1.3)
      run command: ./iimc-hwmcc13 <aig-name>

    3. Temporal Induction Prover (TIP)
      run command: tip <aig-name>

    4. Super Prove
      run command: super_prove <aig-name>

    ACL2 Sedan (ACL2s)

  • bat-executables ( http://www.ccs.neu.edu/home/jmitesh/dissertation/bat-executables )

    This directory containing executables required to generate BAT models and corresponding AIGs using model generators provided in stack-machine and memory-controller directories. Instructions on how to use these executables are given in individual directories.