-
Notifications
You must be signed in to change notification settings - Fork 0
CONCUR 2015
Unfolding-based Partial Order Reduction was the first version of POET awarded the best paper at the conference CONCUR in 2015. The paper is available here! Below are the instructions to reproduce POET's results presented in the paper.
POET can be installed at least up to GHC-8.0.1.
To install POET follow the steps:
-
Install the Haskell Platform.
Test that your installation was successful by running the commands
ghc,cabal, andhappy. -
Install the first release of POET's front-end called simple-c which can be found here
-
Install the first release of POET which can be found here
If you simply interested in running POET the first release also contains binaries for OS X 10.10.2 and ubuntu 18.
The benchmarks used by POET can be found in the repository con-benchmarks. The particular benchmarks used in the CONCUR 2015 paper are here. This directory contains a spreadsheet with the results. Since the poet front-end is still experimental and does not accept the standard C language, for each benchmark there is a version for poet and another for nidhugg.
Both directories contain bash scripts to reproduce the experiments as well as the logs with the information used in the paper. If you are running poet on OS X, you should use this script because of a difference in the argcmd library.
The front-end is composed of two stages:
- Parser:
- Parses the C file into the AST of the Haskell package language-c
- Transforms the AST of language-c into the AST of simple-c
- Transforms the simple-c AST into a more convenient AST that contains the following statements:
- Assignments
- Conditionals: if-then and if-then-else
- Goto: unconditional jumps
- Function calls to the POET API Furthermore, expressions can only contain one global identifier.
- Converter:
- Converts the restricted simple-c AST to the model of computation.
- Computes the independence relation based on Read Write sets.