JavaPathfinder v6.0 (rev 652+) - (C) RIACS/NASA Ames Research Center ====================================================== system under test application: org2/objectweb/dsrg/bpc/demo/Simulator.java arguments: 0 ====================================================== search started: 26/02/12 15:09 first client runs second client runs second client ends first client runs second client runs first client runs first client ends second client ends first client runs first client runs second client runs first client runs first client runs second client runs second client runs second client runs second client ends first client ends second client ends first client runs first client ends first client runs first client runs first client runs second client runs second client runs second client runs second client runs second client ends second client runs first client runs second client ends first client runs first client runs second client runs first client runs first client runs second client runs second client runs second client runs first client ends second client runs second client runs second client ends first client runs second client runs first client runs first client runs first client runs second client runs second client runs second client runs second client runs second client runs second client runs second client runs second client ends second client runs first client runs first client runs second client ends first client runs second client runs second client runs first client runs second client runs second client runs second client runs second client runs second client runs second client runs second client runs second client ends first client runs first client runs first client runs second client ends second client runs first client runs second client runs second client runs first client runs first client runs second client runs second client runs second client runs second client runs second client runs second client runs second client ends first client runs first client runs first client runs second client ends second client runs first client runs second client runs second client runs first client runs first client runs first client ends second client runs second client runs second client runs second client runs second client runs second client runs second client runs second client ends first client runs first client runs second client ends second client runs first client runs second client runs first client runs second client runs second client ends second client runs second client runs second client runs second client runs second client runs second client runs second client runs second client ends first client runs first client runs second client ends second client runs first client runs second client runs second client runs second client runs first client runs first client runs first client runs first client ends second client runs second client runs first client ends second client runs second client runs second client runs second client ends first client ends first client runs first client runs second client ends second client runs second client runs first client runs first client runs second client runs second client ends first client ends second client runs second client runs second client ends first client ends first client runs first client runs second client ends second client runs second client runs first client runs first client runs second client runs second client ends first client ends second client runs second client ends first client ends first client runs second client ends second client runs second client runs second client runs first client runs first client runs first client runs second client runs second client runs second client ends first client ends second client runs second client ends first client ends second client ends second client runs second client runs first client runs first client runs second client runs second client ends first client ends second client runs first client ends second client ends second client runs first client runs first client ends second client ends first client ends second client runs second client ends first client ends second client ends second client runs second client runs first client runs first client runs second client runs second client ends first client ends first client ends second client ends first client ends second client runs second client ends second client runs second client runs first client runs first client runs second client runs second client ends first client ends second client ends first client ends first client ends second client runs second client ends first client ends second client runs second client runs first client runs first client ends second client ends first client ends first client ends second client runs ========potential races======== object id: 36529134 (36529134) field: long org2.objectweb.dsrg.bpc.demo.DataRow_AccountDatabase.PrepaidTime thread id: 1 (Thread-1) instruction: org2.objectweb.dsrg.bpc.demo.AccountDatabaseImpl.AdjustAccountPrepaidTime(AccountDatabaseImpl.java:91) READ [()(1083)] ] instruction: org2.objectweb.dsrg.bpc.demo.AccountDatabaseImpl.AdjustAccountPrepaidTime(AccountDatabaseImpl.java:91) WRITE [()(1083)] ] instruction: org2.objectweb.dsrg.bpc.demo.AccountDatabaseImpl.RechargeAccount(AccountDatabaseImpl.java:140) WRITE [()] ] instruction: org2.objectweb.dsrg.bpc.demo.AccountDatabaseImpl.CreateToken(AccountDatabaseImpl.java:67) READ [()] ] instruction: org2.objectweb.dsrg.bpc.demo.AccountDatabaseImpl.RechargeAccount(AccountDatabaseImpl.java:140) READ [()] ] instruction: org2.objectweb.dsrg.bpc.demo.AccountDatabaseImpl.CreateToken(AccountDatabaseImpl.java:66) READ [()] ] instruction: org2.objectweb.dsrg.bpc.demo.AccountDatabaseImpl.CreateToken(AccountDatabaseImpl.java:67) WRITE [()] ] thread id: 2 (Thread-2) instruction: org2.objectweb.dsrg.bpc.demo.AccountDatabaseImpl.RechargeAccount(AccountDatabaseImpl.java:140) WRITE [()] ] instruction: org2.objectweb.dsrg.bpc.demo.AccountDatabaseImpl.RechargeAccount(AccountDatabaseImpl.java:140) READ [()] ] ============================ monitor id 1083 org2.objectweb.dsrg.bpc.demo.IpAddressManagerImpl object id: 143014233 (143014233) field: java.math.BigDecimal org2.objectweb.dsrg.bpc.demo.DataRow_CardCenter.Balance thread id: 1 (Thread-1) instruction: org2.objectweb.dsrg.bpc.demo.CardCenterImpl.Withdraw(CardCenterImpl.java:35) READ [()] ] instruction: org2.objectweb.dsrg.bpc.demo.CardCenterImpl.Withdraw(CardCenterImpl.java:28) READ [()] ] instruction: org2.objectweb.dsrg.bpc.demo.CardCenterImpl.Withdraw(CardCenterImpl.java:35) WRITE [()] ] thread id: 2 (Thread-2) instruction: org2.objectweb.dsrg.bpc.demo.CardCenterImpl.Withdraw(CardCenterImpl.java:35) READ [()] ] instruction: org2.objectweb.dsrg.bpc.demo.CardCenterImpl.Withdraw(CardCenterImpl.java:28) READ [()] ] instruction: org2.objectweb.dsrg.bpc.demo.CardCenterImpl.Withdraw(CardCenterImpl.java:35) WRITE [()] ] ============================ ======== sumary ======== 1 >Potential race for field org2.objectweb.dsrg.bpc.demo.DataRow_AccountDatabase.PrepaidTime write: [Thread-1] org2.objectweb.dsrg.bpc.demo.AccountDatabaseImpl.AdjustAccountPrepaidTime read: [Thread-2] org2.objectweb.dsrg.bpc.demo.AccountDatabaseImpl.RechargeAccount < 2 >Potential race for field org2.objectweb.dsrg.bpc.demo.DataRow_AccountDatabase.PrepaidTime write: [Thread-1] org2.objectweb.dsrg.bpc.demo.AccountDatabaseImpl.RechargeAccount read: [Thread-2] org2.objectweb.dsrg.bpc.demo.AccountDatabaseImpl.RechargeAccount < 3 >Potential race for field org2.objectweb.dsrg.bpc.demo.DataRow_AccountDatabase.PrepaidTime write: [Thread-1] org2.objectweb.dsrg.bpc.demo.AccountDatabaseImpl.CreateToken read: [Thread-2] org2.objectweb.dsrg.bpc.demo.AccountDatabaseImpl.RechargeAccount < 4 >Potential race for field org2.objectweb.dsrg.bpc.demo.DataRow_CardCenter.Balance write: [Thread-1] org2.objectweb.dsrg.bpc.demo.CardCenterImpl.Withdraw read: [Thread-2] org2.objectweb.dsrg.bpc.demo.CardCenterImpl.Withdraw < ====================================================== results no errors detected ====================================================== statistics elapsed time: 00:00:05 states: new=2059, visited=1738, backtracked=3797, end=21 search: maxDepth=26, constraints hit=0 choice generators: thread=1806 (signal=0, lock=490, shared ref=1174), data=0 heap: new=12648, released=6593, max live=1334, gc-cycles=3787 instructions: 756254 max memory: 212MB loaded code: classes=177, methods=2543 ====================================================== search finished: 26/02/12 15:09