PV2 ⊧ Islagenerates a state graph or a test case from an architecture spec

Tool to evaluate relaxed-memory behaviour of instruction set architectures w.r.t. arbitrary axiomatic memory models

Application domain/field

• Instruction-set architecture (ISA) semantics
• Concurrency models
• Relaxed-memory concurrency models
• Processor architecture
• Symbolic execution

Expected input

• Architecture (e.g. aarch64.ir)
• Configuration file that defines e.g. the initial state (.toml file)
• Memory model specified in the Cat language (.cat file)

Format:

• Architecture: Pre-compiled Sail representation, .ir file. For some architectures compiled SAIL snapshots are available via https://github.com/rems-project/isla-snapshots
• Configuration file: .toml file
• Model: Cat language, .cat file

Comments

License: BSD 2-Clause