Skip to content

Experimental static analyser for concurrent programs within the TSO relaxed memory model.

Notifications You must be signed in to change notification settings

thizanne/cormoran

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 

Repository files navigation

Cormoran

A Concurrent TSO-Relaxed Memory program static Analyser.

https://cloud.githubusercontent.com/assets/1719378/7755936/f85888d4-fff7-11e4-80fa-1f9786e33982.jpg

How to build

ocamlbuild cormoran.native

How to run

  • With default options: ./cormoran.native filename
  • For more options: ./cormoran.native --help

How to write source files

See the directory tests/ for syntax examples.

Precautions:

  • Expressions must contain at most one shared variable.
  • Expressions in conditions must not contain any shared variable.

The typing pass should explain clearly any other issue when writing a syntactically correct but semantically wrong file.

Litmus tests syntax is also accepted with the --litmus option. Use them with caution: they are expected to be correctly written (as they are usually automatically generated) and won’t be typechecked.

Dependencies

  • apron
  • batteries
  • bddapron
  • cmdliner
  • menhir
  • ocamlgraph
  • ppx_deriving
  • ppx_deriving_cmdliner

About

Experimental static analyser for concurrent programs within the TSO relaxed memory model.

Resources

Stars

Watchers

Forks

Packages

No packages published