csiluszyk/simple-program-verifier

Thread safty verifier of simple programs written in Prolog.

Thread-safty verifier

Thread safty verifier of simple programs.

Project structure

• verify.pl - program runner,
• verifier.pl - source code of the verifier,
• dekker.pl - Dekker's algorithm example,
• hyman.pl - Hyman's mutual exclusion algorithm example,
• peterson.pl - Peterson's algorithm example,
• unsafe.pl - thread-unsafe example,
• example.pl - thread-safe if number of processors <= 2 example.

Grammar of simple programs

Exp         ::=  ExpVal | ExpVal ExpOper ExpVal
ExpVal      ::=  number | Variable
Variable    ::=  ident | arr(ident, Exp)
ExpOper     ::=  + | - | * | /
BoolExp     ::=  ExpVal BoolOper ExpVal
BoolOper    ::=  < | = | <>

Running tests

Requirements

• SWI-Prolog

Example runs:

• ./verify.pl 2 peterson.pl - correct,
• ./verify.pl 3 peterson.pl - incorrect,