JavaPathfinder v6.0 (rev 652+) - (C) RIACS/NASA Ames Research Center ====================================================== system under test application: Airline/Main.java arguments: 20 5 ====================================================== search started: 26/02/12 14:38 20 15 ========potential races======== object id: 154712557 (154712557) field: boolean Airline.Bug.StopSales thread id: 0 (main) instruction: Airline.Bug.(Bug.java:42) READ [()] ] thread id: 9 (Thread-9) instruction: Airline.Bug.run(Bug.java:66) WRITE [()] ] thread id: 10 (Thread-10) instruction: Airline.Bug.run(Bug.java:66) WRITE [()] ] thread id: 11 (Thread-11) instruction: Airline.Bug.run(Bug.java:66) WRITE [()] ] thread id: 12 (Thread-12) instruction: Airline.Bug.run(Bug.java:66) WRITE [()] ] thread id: 13 (Thread-13) instruction: Airline.Bug.run(Bug.java:66) WRITE [()] ] thread id: 14 (Thread-14) instruction: Airline.Bug.run(Bug.java:66) WRITE [()] ] thread id: 15 (Thread-15) instruction: Airline.Bug.run(Bug.java:66) WRITE [()] ] thread id: 16 (Thread-16) instruction: Airline.Bug.run(Bug.java:66) WRITE [()] ] thread id: 17 (Thread-17) instruction: Airline.Bug.run(Bug.java:66) WRITE [()] ] thread id: 18 (Thread-18) instruction: Airline.Bug.run(Bug.java:66) WRITE [()] ] thread id: 19 (Thread-19) instruction: Airline.Bug.run(Bug.java:66) WRITE [()] ] thread id: 20 (Thread-20) instruction: Airline.Bug.run(Bug.java:66) WRITE [()] ] ============================ (static field) field: static int Airline.Bug.Num_Of_Seats_Sold thread id: 0 (main) instruction: Airline.Bug.(Bug.java:55) READ [()] ] thread id: 1 (Thread-1) instruction: Airline.Bug.run(Bug.java:64) WRITE [()] ] instruction: Airline.Bug.run(Bug.java:65) READ [()] ] instruction: Airline.Bug.run(Bug.java:64) READ [()] ] thread id: 2 (Thread-2) instruction: Airline.Bug.run(Bug.java:64) WRITE [()] ] instruction: Airline.Bug.run(Bug.java:65) READ [()] ] instruction: Airline.Bug.run(Bug.java:64) READ [()] ] thread id: 3 (Thread-3) instruction: Airline.Bug.run(Bug.java:64) WRITE [()] ] instruction: Airline.Bug.run(Bug.java:65) READ [()] ] instruction: Airline.Bug.run(Bug.java:64) READ [()] ] thread id: 4 (Thread-4) instruction: Airline.Bug.run(Bug.java:64) WRITE [()] ] instruction: Airline.Bug.run(Bug.java:65) READ [()] ] instruction: Airline.Bug.run(Bug.java:64) READ [()] ] thread id: 5 (Thread-5) instruction: Airline.Bug.run(Bug.java:64) WRITE [()] ] instruction: Airline.Bug.run(Bug.java:65) READ [()] ] instruction: Airline.Bug.run(Bug.java:64) READ [()] ] thread id: 6 (Thread-6) instruction: Airline.Bug.run(Bug.java:64) WRITE [()] ] instruction: Airline.Bug.run(Bug.java:65) READ [()] ] instruction: Airline.Bug.run(Bug.java:64) READ [()] ] thread id: 7 (Thread-7) instruction: Airline.Bug.run(Bug.java:64) WRITE [()] ] instruction: Airline.Bug.run(Bug.java:65) READ [()] ] instruction: Airline.Bug.run(Bug.java:64) READ [()] ] thread id: 8 (Thread-8) instruction: Airline.Bug.run(Bug.java:64) WRITE [()] ] instruction: Airline.Bug.run(Bug.java:65) READ [()] ] instruction: Airline.Bug.run(Bug.java:64) READ [()] ] thread id: 9 (Thread-9) instruction: Airline.Bug.run(Bug.java:64) WRITE [()] ] instruction: Airline.Bug.run(Bug.java:65) READ [()] ] instruction: Airline.Bug.run(Bug.java:64) READ [()] ] thread id: 10 (Thread-10) instruction: Airline.Bug.run(Bug.java:64) WRITE [()] ] instruction: Airline.Bug.run(Bug.java:65) READ [()] ] instruction: Airline.Bug.run(Bug.java:64) READ [()] ] thread id: 11 (Thread-11) instruction: Airline.Bug.run(Bug.java:64) WRITE [()] ] instruction: Airline.Bug.run(Bug.java:65) READ [()] ] instruction: Airline.Bug.run(Bug.java:64) READ [()] ] thread id: 12 (Thread-12) instruction: Airline.Bug.run(Bug.java:64) WRITE [()] ] instruction: Airline.Bug.run(Bug.java:65) READ [()] ] instruction: Airline.Bug.run(Bug.java:64) READ [()] ] thread id: 13 (Thread-13) instruction: Airline.Bug.run(Bug.java:64) WRITE [()] ] instruction: Airline.Bug.run(Bug.java:65) READ [()] ] instruction: Airline.Bug.run(Bug.java:64) READ [()] ] thread id: 14 (Thread-14) instruction: Airline.Bug.run(Bug.java:64) WRITE [()] ] instruction: Airline.Bug.run(Bug.java:65) READ [()] ] instruction: Airline.Bug.run(Bug.java:64) READ [()] ] thread id: 15 (Thread-15) instruction: Airline.Bug.run(Bug.java:64) WRITE [()] ] instruction: Airline.Bug.run(Bug.java:65) READ [()] ] instruction: Airline.Bug.run(Bug.java:64) READ [()] ] thread id: 16 (Thread-16) instruction: Airline.Bug.run(Bug.java:64) WRITE [()] ] instruction: Airline.Bug.run(Bug.java:65) READ [()] ] instruction: Airline.Bug.run(Bug.java:64) READ [()] ] thread id: 17 (Thread-17) instruction: Airline.Bug.run(Bug.java:64) WRITE [()] ] instruction: Airline.Bug.run(Bug.java:65) READ [()] ] instruction: Airline.Bug.run(Bug.java:64) READ [()] ] thread id: 18 (Thread-18) instruction: Airline.Bug.run(Bug.java:64) WRITE [()] ] instruction: Airline.Bug.run(Bug.java:65) READ [()] ] instruction: Airline.Bug.run(Bug.java:64) READ [()] ] thread id: 19 (Thread-19) instruction: Airline.Bug.run(Bug.java:64) WRITE [()] ] instruction: Airline.Bug.run(Bug.java:65) READ [()] ] instruction: Airline.Bug.run(Bug.java:64) READ [()] ] thread id: 20 (Thread-20) instruction: Airline.Bug.run(Bug.java:64) WRITE [()] ] instruction: Airline.Bug.run(Bug.java:65) READ [()] ] instruction: Airline.Bug.run(Bug.java:64) READ [()] ] ============================ ======== sumary ======== 1 >Potential race for field Airline.Bug.StopSales write: [Thread-9] Airline.Bug.run read: [main] Airline.Bug. < 2 >Potential race for field Airline.Bug.Num_Of_Seats_Sold write: [Thread-1] Airline.Bug.run read: [main] Airline.Bug. < 3 >Potential race for field Airline.Bug.Num_Of_Seats_Sold write: [Thread-1] Airline.Bug.run read: [Thread-2] Airline.Bug.run < ====================================================== results no errors detected ====================================================== statistics elapsed time: 00:00:05 states: new=3053, visited=13971, backtracked=16988, end=12 search: maxDepth=42, constraints hit=0 choice generators: thread=3053 (signal=0, lock=2, shared ref=0), data=0 heap: new=483, released=1092, max live=434, gc-cycles=17024 instructions: 228361 max memory: 167MB loaded code: classes=81, methods=1323 ====================================================== search finished: 26/02/12 14:38