This page describes the basic steps for using Poirot to find bugs in concurrent programs. We will walk through the bank account example that is in the Poirot4C\examples\accounts directory. The file account.c contains a simple implementation of a bank account from which one can withdraw or deposit concurrently.

Step 1. Annotate concurrency in your program

Poirot currently does not infer concurrency present in a program. One has to explicitly mark thread creation and join operations. Thread creation is marked with "__async_call" macro. For instance, the following lines in poirot_main spawn two threads:

__async_call t1 = deposit_test(acc, y);

__async_call t2 = withdraw_test(acc, z, &withdrawn);

The return values t1 and t2 are the thread IDs of the corresponding thread that is spawned.

Thread join operation can be performed using the POIROT_THREAD_JOIN(int) macro that expects a thread ID as its argument. These annotation macros, and other useful ones, are declared in Poirot4C\include\poirot.h. See Poirot4C\examples\account\locks.h for how they can be used.

Step 2. Mark the property to be checked using assertions

The macro POIROT_ASSERT(bool) must be used to mark an assertion that is to be checked by poirot. This assertion can be inserted anywhere in the program, even multiple times. Note that poirot assumes that the main procedure of the program is called "poirot_main" (so that one does not have to change their existing main procedure).

For example, in the bank account example, the invariant is that if the withdraw operation succeeded, then the resulting balance should be "original + deposited - withdrawn". The corresponding assertion for checking this invariant is at the end of poirot_main:

POIROT_ASSERT(!withdrawn || read(acc) == x + y - z);

Step 3. Get ready to compile your program

One must pass the following flags to the compiler: "/I$(POIROT_ROOT)\Poirot4C\include" and "/analyze:plugin $(POIROT_ROOT)\Poirot4C\havoc\EspFe.dll". The former is to be able to find "poirot.h" and the latter is to allow Havoc to gather up all the source files. One must also use "nmake" to compiler their program. See the Makefile included in examples\account:

ANALYZE_OPT = /analyze:plugin $(POIROT_ROOT)\Poirot4C\havoc\EspFe.dll

DRIVER_OPT = /I$(POIROT_ROOT)\Poirot4C\include

...

cl $(ANALYZE_OPT) $(DRIVER_OPT) *.c

Step 4. Run poirot!

First, go to poirot's install directory and run setup.cmd. This will set up the environment for poirot. Next, go to your source directory (i.e., the directory where you run nmake to compile your program), and run poirot4c.bat. Example: go to examples\account and run poirot4c.bat. No error would be displayed. Now open account.c and uncomment the line "// #define BUG2". Run poirot4c.bat again to see the error trace being displayed.

By default, poirot checks a program with a context bound of 2, a loop unrolling bound of 1, and starts exploration from poirot_main. This can be changed, for instance, by running poirot4c.bat with the following arguments:

> poirot4c.bat /k:4 /recursionBound:10 /main:my_main