E.4 How to Use Promela
Keywords: perfbook_html

#
E.4 How to Use Promela

Given a source file `qrcu.spin`, one can use the following commands:

- `spin -a qrcu.spin` Create a file pan.c that fully searches the state machine.
- `cc -DSAFETY -o pan pan.c` Compile the generated state-machine search. The -DSAFETY generates optimizations that are appropriate if you have only assertions (and perhaps never statements). If you have liveness, fairness, or forward-progress checks, you may need to compile without -DSAFETY. If you leave off -DSAFETY when you could have used it, the program will let you know.

  The optimizations produced by -DSAFETY greatly speed things up, so you should use it when you can. An example situation where you cannot use -DSAFETY is when checking for livelocks (AKA ``non-progress cycles'') via -DNP.

- `./pan` This actually searches the state space. The number of states can reach into the tens of millions with very small state machines, so you will need a machine with large memory. For example, qrcu.spin with 3 readers and 2 updaters required 2.7GB of memory.

  If you aren't sure whether your machine has enough memory, run top in one window and ./pan in another. Keep the focus on the ./pan window so that you can quickly kill execution if need be. As soon as CPU time drops much below 100%, kill ./pan. If you have removed focus from the window running ./pan, you may wait a long time for the windowing system to grab enough memory to do anything for you.

  Don't forget to capture the output, especially if you are working on a remote machine,

  If your model includes forward-progress checks, you will likely need to enable ``weak fairness'' via the -f command-line argument to ./pan. If your forward-progress checks involve accept labels, you will also need the -a argument.

- `spin -t -p qrcu.spin` Given trail file output by a run that encountered an error, output the sequence of steps leading to that error. The -g flag will also include the values of changed global variables, and the -l flag will also include the values of changed local variables.

Subsections

- E.4.1 Promela Peculiarities
- E.4.2 Promela Coding Tricks