PV5 ⊧ Nidhugggiven a program and a memory model, reports assertion violations

Stateless model checker (SMC) for C/C++ programs

Application domain/field

• Model checking
• Stateless model checking
• Concurrency
• Concurrent programs
• Relaxed memory models

Type of tool

Model checker

Expected input

• Multithreaded C/C++ program
• Each thread should be deterministic when run in isolation.
• The concurrency should be implemented with pthreads.
• Memory model

Format:

• Program: .ll file (LLVM assembly code)
• Memory model: This is passed as an argument when calling Nidhugg. It can be one of the following: --sc, --tso, --pso, --power, --arm.

Expected output

It will indicate an error or state that no errors were found. The errors can be either assertion violations or robustness violations (e.g. segmentation faults).

Internals

• It supports the following memory models: SC, TSO, PSO, POWER and ARM.
• Nidhugg explores the possible executions to find bugs. It does this such that it will not explore executions that are equivalent to each other.

Comments

License: GPL v3.0