Data-races are an important kind of concurrency error found in shared-memory programs. Software model checking is a popular approach to find them: it explores the state-space of a program reachable from an informed test driver in seek of errors. Unfortunately, the approach can be very expensive for scenarios that produce very large state-spaces. This paper proposes Rabbit, a novel approach to find data-races that complements model-checking by efficiently reporting precise warnings during state-space exploration (SSE). Rabbit uses coverage information obtained across the different schedules produced during SSE to predict likely racy memory accesses. It builds on the observation that, during SSE, memory accesses are covered much sooner than the actual race. We evaluated Rabbit on 33 different scenarios of race, involving a total of 23 distinct application subjects of various sources and sizes. Results indicate that Rabbit reports race warnings very soon compared to the time the model checker detects the race (for 78\% of the cases Rabbit reports a true warning of race within 5s of SSE), that the warnings it reports include few false alarms, and that the overhead on overall exploration time is, on average, very low.
The output presented in red is produced by rabbit, its the main results of rabbit
analysis. It demonstrated all access in a field(identified by a field name) of an
object(identified by the rabbit object id). for the first object id '235815501',
it's refer to an instance of the class Account. The data point out all access in
the field Account.Account.amount by different threads, as well the
method name that does the access, the code location, the operation type(WRITE or
READ) and objects ids of locks held by thread during the access.
The output presented in green color is also produced by rabbit, its is just an easy-to-see extracted information of the red colored part.
The brown colored text is produced by JPF. its presents wheter JPF found an error or not, the total search time, and other data during the state space exploration
JavaPathfinder v6.0 (rev 652+) - (C) RIACS/NASA Ames Research Center ====================================================== system under test application: Account/Main.java arguments: 7 ====================================================== search started: 26/02/12 11:48 ========potential races======== object id: 235815501 (235815501) field: double Account.Account.amount thread id: 1 (Thread-1) instruction: Account.Account.withdraw(Account.java:19) WRITE [(382)]] instruction: Account.Account.transfer(Account.java:23) READ [(382)]] instruction: Account.Account.transfer(Account.java:23) WRITE [(382)]] instruction: Account.Account.withdraw(Account.java:19) READ [(382)]] instruction: Account.Account.depsite(Account.java:15) READ [(382)]] instruction: Account.Account.depsite(Account.java:15) WRITE [(382)]] thread id: 6 (Thread-6) instruction: Account.Account.transfer(Account.java:31) WRITE [(382, 430)] ] instruction: Account.Account.transfer(Account.java:31) READ [(382, 430)] ] thread id: 7 (Thread-7) instruction: Account.Account.transfer(Account.java:31) WRITE [(382, 437)] ] instruction: Account.Account.transfer(Account.java:31) READ [(382, 437)] ] ============================ monitor id 382 Account.Account monitor id 430 Account.Account monitor id 437 Account.Account ... more ... ======== sumary ======== 1 >Potential race for field Account.Account.amount write: [Thread-4] Account.Account.transfer read: [Thread-5] Account.Account.transfer < ... more ... ====================================================== results no errors detected ====================================================== statistics elapsed time: 00:00:05 states: new=7460, visited=11167, backtracked=18552, end=5 search: maxDepth=126, constraints hit=0 choice generators: thread=7459 (signal=0,lock=1411, shared ref=4524), data=0 heap: new=438, released=237, max live=438, gc-cycles=16390 instructions: 154355 max memory: 106MB loaded code: classes=84, methods=1328 ======================================================search finished: 26/02/12 11:48
| subject | # threads | rabbit | JPF Time |
|---|---|---|---|
| account | 7 | 3(3) | 3m24s |
| account | 8 | 3(3) | 4h9m41s |
| account-pecan | 2 | 0(0) | 14s |
| account-pecan | 10 | 1(1) | 41s |
| airline | 19 | 2(2) | 7m01s |
| airline | 20 | 2(2) | 17m48s |
| alarmClock | 8 | 1(0) | 7m01s |
| alarmClock | 9 | 1(0) | 31m25s |
| cache4j-pecan | 2 | 2(1) | 1s |
| cache4j-pecan | 2 | 2(1) | OME 2h38m16s |
| cocome | 4 | 6(6) | 5h34m |
| cocome2 | 4 | 2(2) | 1s |
| credemo | 5 | 1(1) | 36s |
| credemo2 | 5 | 5(5) | 28s |
| daisy2-1 | 2 | 1-1 | 19m24s |
| daisy2-1 | 2 | 1-1 | 4s |
| lang | 10 | 0-0 | OME 20m07s |
| monte carlo | 5 | 0-0 | 20s |
| moldyn | 5 | 1-1 | OME 4m26s |
| moldyn-2 | 5 | 0-0 | OME 4m30s |
| pool-1 | 3 | 2-1 | OME 3h59m01s |
| pool-2 | 3 | 2-1 | 2m31s |
| jpapa | 15 | 0(0) | OME 2H27min |
| raxExtended | 13 | 2(1) | 8m16s |
| raxExtended | 15 | 2(1) | 38m23s |
| shop | 4 | 1-1 | OME 21h05m00s |
| twoStages | 17 | 3(1) | 6m33s |
| twoStages | 18 | 3(1) | 29m45s |
| tsp | 3 | 4(4) | 9m16s |
| weblech | 5 | 2(2) | 17m54s |
| wrongLock | 18 | 3(1) | 6m07 |
| wrongLock | 19 | 3(1) | 9m10s |
listener=br.cin.ufpe.rabbit.ObjectIdListener,br.cin.ufpe.rabbit.RabbitListener
in your JPF property
file.
To download the latest realeases of rabbit: https://code.google.com/p/jpf-rabbit/