*** Violation Patterns [ID - Memory Location - Line Number - Thread - Access Type] *** -------------------------------------- *** RACE *** 142925 "spec.jbb.TimerData.btps" 362 10 WRITE * 143218 "spec.jbb.TimerData.btps" 363 11 READ *** *** RACE *** 143553 "spec.jbb.TimerData.minimumTime" 471 1 READ * 143080 "spec.jbb.TimerData.minimumTime" 321 11 WRITE *** *** RACE *** 142926 "spec.jbb.TimerData.btps" 363 10 READ * 143217 "spec.jbb.TimerData.btps" 362 11 WRITE *** *** RACE *** 142777 "spec.jbb.TimerData.minimumTime" 321 10 WRITE * 143080 "spec.jbb.TimerData.minimumTime" 321 11 WRITE *** *** RACE *** 143630 "spec.jbb.TimerData.maximumTime" 595 1 READ * 143082 "spec.jbb.TimerData.maximumTime" 324 11 WRITE *** *** RACE *** 143571 "spec.jbb.TimerData.btps" 503 1 READ * 143217 "spec.jbb.TimerData.btps" 362 11 WRITE *** *** RACE *** 142912 "spec.jbb.TimerData.min_transaction_count" 331 10 WRITE * 143204 "spec.jbb.TimerData.min_transaction_count" 330 11 READ *** *** RACE *** 142922 "spec.jbb.TimerData.tpmc" 344 10 WRITE * 143215 "spec.jbb.TimerData.tpmc" 345 11 READ *** *** RACE *** 143622 "spec.jbb.TimerData.minimumTime" 579 1 READ * 143080 "spec.jbb.TimerData.minimumTime" 321 11 WRITE *** *** RACE *** 143558 "spec.jbb.TimerData.minimumTime" 479 1 READ * 143080 "spec.jbb.TimerData.minimumTime" 321 11 WRITE *** *** RACE *** 4657 "spec.jbb.TransactionManager.mode" 25 10 WRITE * 5046 "spec.jbb.TransactionManager.mode" 181 1 WRITE *** *** RACE *** 141395 "spec.jbb.Company.threadsDoneCount" 475 1 READ * 141610 "spec.jbb.Company.threadsDoneCount" 244 10 WRITE *** *** RACE *** 143629 "spec.jbb.TimerData.minimumTime" 593 1 READ * 143080 "spec.jbb.TimerData.minimumTime" 321 11 WRITE *** *** RACE *** 143609 "spec.jbb.TimerData.maximumTime" 553 1 READ * 143082 "spec.jbb.TimerData.maximumTime" 324 11 WRITE *** *** RACE *** 143644 "spec.jbb.TimerData.maximumTime" 623 1 READ * 143082 "spec.jbb.TimerData.maximumTime" 324 11 WRITE *** *** RACE *** 143648 "spec.jbb.TimerData.btps" 631 1 READ * 143217 "spec.jbb.TimerData.btps" 362 11 WRITE *** *** RACE *** 142911 "spec.jbb.TimerData.min_transaction_count" 330 10 READ * 143205 "spec.jbb.TimerData.min_transaction_count" 331 11 WRITE *** *** RACE *** 142778 "spec.jbb.TimerData.maximumTime" 323 10 READ * 143082 "spec.jbb.TimerData.maximumTime" 324 11 WRITE *** *** RACE *** 142927 "spec.jbb.Company.stopThreadsCount" 292 10 READ * 143220 "spec.jbb.Company.stopThreadsCount" 292 11 WRITE *** *** RACE *** 143615 "spec.jbb.TimerData.minimumTime" 565 1 READ * 143080 "spec.jbb.TimerData.minimumTime" 321 11 WRITE *** *** RACE *** 142776 "spec.jbb.TimerData.minimumTime" 319 10 READ * 143080 "spec.jbb.TimerData.minimumTime" 321 11 WRITE *** *** RACE *** 143608 "spec.jbb.TimerData.minimumTime" 551 1 READ * 143080 "spec.jbb.TimerData.minimumTime" 321 11 WRITE *** *** RACE *** 142912 "spec.jbb.TimerData.min_transaction_count" 331 10 WRITE * 143205 "spec.jbb.TimerData.min_transaction_count" 331 11 WRITE *** *** RACE *** 142924 "spec.jbb.TimerData.btps" 362 10 READ * 143217 "spec.jbb.TimerData.btps" 362 11 WRITE *** *** RACE *** 143563 "spec.jbb.TimerData.minimumTime" 487 1 READ * 143080 "spec.jbb.TimerData.minimumTime" 321 11 WRITE *** *** RACE *** 142777 "spec.jbb.TimerData.minimumTime" 321 10 WRITE * 143078 "spec.jbb.TimerData.minimumTime" 319 11 READ *** *** RACE *** 143206 "spec.jbb.TimerData.max_transaction_count" 333 11 READ * 142914 "spec.jbb.TimerData.max_transaction_count" 334 10 WRITE *** *** RACE *** 143543 "spec.jbb.TimerData.minimumTime" 455 1 READ * 143080 "spec.jbb.TimerData.minimumTime" 321 11 WRITE *** *** RACE *** 143651 "spec.jbb.TimerData.min_transaction_count" 657 1 READ * 143205 "spec.jbb.TimerData.min_transaction_count" 331 11 WRITE *** *** RACE *** 143623 "spec.jbb.TimerData.maximumTime" 581 1 READ * 143082 "spec.jbb.TimerData.maximumTime" 324 11 WRITE *** *** RACE *** 142914 "spec.jbb.TimerData.max_transaction_count" 334 10 WRITE * 143206 "spec.jbb.TimerData.max_transaction_count" 333 11 READ *** *** RACE *** 143569 "spec.jbb.TimerData.maximumTime" 497 1 READ * 143082 "spec.jbb.TimerData.maximumTime" 324 11 WRITE *** *** RACE *** 142923 "spec.jbb.TimerData.tpmc" 345 10 READ * 143214 "spec.jbb.TimerData.tpmc" 344 11 WRITE *** *** RACE *** 142921 "spec.jbb.TimerData.tpmc" 344 10 READ * 143214 "spec.jbb.TimerData.tpmc" 344 11 WRITE *** *** RACE *** 143636 "spec.jbb.TimerData.minimumTime" 607 1 READ * 143080 "spec.jbb.TimerData.minimumTime" 321 11 WRITE *** *** RACE *** 142779 "spec.jbb.TimerData.maximumTime" 324 10 WRITE * 143082 "spec.jbb.TimerData.maximumTime" 324 11 WRITE *** *** RACE *** 143564 "spec.jbb.TimerData.maximumTime" 489 1 READ * 143082 "spec.jbb.TimerData.maximumTime" 324 11 WRITE *** *** RACE *** 142308 "spec.jbb.Company.stopThreadsCount" 485 1 READ * 142928 "spec.jbb.Company.stopThreadsCount" 292 10 WRITE *** *** RACE *** 4850 "spec.jbb.Company.initThreadsCount" 388 1 READ * 5038 "spec.jbb.Company.initThreadsCount" 206 11 WRITE *** *** RACE *** 143643 "spec.jbb.TimerData.minimumTime" 621 1 READ * 143080 "spec.jbb.TimerData.minimumTime" 321 11 WRITE *** *** RACE *** 143559 "spec.jbb.TimerData.maximumTime" 481 1 READ * 143082 "spec.jbb.TimerData.maximumTime" 324 11 WRITE *** *** RACE *** 143637 "spec.jbb.TimerData.maximumTime" 609 1 READ * 143082 "spec.jbb.TimerData.maximumTime" 324 11 WRITE *** *** RACE *** 143568 "spec.jbb.TimerData.minimumTime" 495 1 READ * 143080 "spec.jbb.TimerData.minimumTime" 321 11 WRITE *** *** RACE *** 143528 "spec.jbb.TimerData.min_transaction_count" 646 1 READ * 143205 "spec.jbb.TimerData.min_transaction_count" 331 11 WRITE *** *** RACE *** 143548 "spec.jbb.TimerData.minimumTime" 463 1 READ * 143080 "spec.jbb.TimerData.minimumTime" 321 11 WRITE *** *** RACE *** 143554 "spec.jbb.TimerData.maximumTime" 473 1 READ * 143082 "spec.jbb.TimerData.maximumTime" 324 11 WRITE *** *** RACE *** 142779 "spec.jbb.TimerData.maximumTime" 324 10 WRITE * 143081 "spec.jbb.TimerData.maximumTime" 323 11 READ *** *** RACE *** 143549 "spec.jbb.TimerData.maximumTime" 465 1 READ * 143082 "spec.jbb.TimerData.maximumTime" 324 11 WRITE *** *** RACE *** 143616 "spec.jbb.TimerData.maximumTime" 567 1 READ * 143082 "spec.jbb.TimerData.maximumTime" 324 11 WRITE *** *** RACE *** 143544 "spec.jbb.TimerData.maximumTime" 457 1 READ * 143082 "spec.jbb.TimerData.maximumTime" 324 11 WRITE *** *** RACE *** 143527 "spec.jbb.TimerData.min_transaction_count" 645 1 READ * 143205 "spec.jbb.TimerData.min_transaction_count" 331 11 WRITE *** *** RACE *** 4839 "spec.jbb.Company.initThreadsCount" 206 10 READ * 5038 "spec.jbb.Company.initThreadsCount" 206 11 WRITE *** *** RACE *** 5046 "spec.jbb.TransactionManager.mode" 181 1 WRITE * 4657 "spec.jbb.TransactionManager.mode" 25 10 WRITE *** *** AV-I --- 143564 "spec.jbb.TimerData.maximumTime" 489 1 READ * 143082 "spec.jbb.TimerData.maximumTime" 324 11 WRITE * 143569 "spec.jbb.TimerData.maximumTime" 497 1 READ *** *** AV-I --- 143559 "spec.jbb.TimerData.maximumTime" 481 1 READ * 143082 "spec.jbb.TimerData.maximumTime" 324 11 WRITE * 143569 "spec.jbb.TimerData.maximumTime" 497 1 READ *** *** AV-I --- 143554 "spec.jbb.TimerData.maximumTime" 473 1 READ * 143082 "spec.jbb.TimerData.maximumTime" 324 11 WRITE * 143569 "spec.jbb.TimerData.maximumTime" 497 1 READ *** *** AV-I --- 143553 "spec.jbb.TimerData.minimumTime" 471 1 READ * 143080 "spec.jbb.TimerData.minimumTime" 321 11 WRITE * 143568 "spec.jbb.TimerData.minimumTime" 495 1 READ *** *** AV-I --- 143548 "spec.jbb.TimerData.minimumTime" 463 1 READ * 143080 "spec.jbb.TimerData.minimumTime" 321 11 WRITE * 143553 "spec.jbb.TimerData.minimumTime" 471 1 READ *** *** AV-I --- 143548 "spec.jbb.TimerData.minimumTime" 463 1 READ * 143080 "spec.jbb.TimerData.minimumTime" 321 11 WRITE * 143568 "spec.jbb.TimerData.minimumTime" 495 1 READ *** *** AV-I --- 143543 "spec.jbb.TimerData.minimumTime" 455 1 READ * 143080 "spec.jbb.TimerData.minimumTime" 321 11 WRITE * 143548 "spec.jbb.TimerData.minimumTime" 463 1 READ *** *** AV-I --- 143543 "spec.jbb.TimerData.minimumTime" 455 1 READ * 143080 "spec.jbb.TimerData.minimumTime" 321 11 WRITE * 143553 "spec.jbb.TimerData.minimumTime" 471 1 READ *** *** AV-I --- 143543 "spec.jbb.TimerData.minimumTime" 455 1 READ * 143080 "spec.jbb.TimerData.minimumTime" 321 11 WRITE * 143568 "spec.jbb.TimerData.minimumTime" 495 1 READ *** *** AV-I --- 4839 "spec.jbb.Company.initThreadsCount" 206 10 READ * 5038 "spec.jbb.Company.initThreadsCount" 206 11 WRITE * 4840 "spec.jbb.Company.initThreadsCount" 206 10 WRITE *** *** AV-I --- 143558 "spec.jbb.TimerData.minimumTime" 479 1 READ * 143080 "spec.jbb.TimerData.minimumTime" 321 11 WRITE * 143568 "spec.jbb.TimerData.minimumTime" 495 1 READ *** *** AV-I --- 143563 "spec.jbb.TimerData.minimumTime" 487 1 READ * 143080 "spec.jbb.TimerData.minimumTime" 321 11 WRITE * 143568 "spec.jbb.TimerData.minimumTime" 495 1 READ *** *** AV-I --- 143544 "spec.jbb.TimerData.maximumTime" 457 1 READ * 143082 "spec.jbb.TimerData.maximumTime" 324 11 WRITE * 143569 "spec.jbb.TimerData.maximumTime" 497 1 READ *** *** AV-I --- 143544 "spec.jbb.TimerData.maximumTime" 457 1 READ * 143082 "spec.jbb.TimerData.maximumTime" 324 11 WRITE * 143549 "spec.jbb.TimerData.maximumTime" 465 1 READ *** *** AV-I --- 143549 "spec.jbb.TimerData.maximumTime" 465 1 READ * 143082 "spec.jbb.TimerData.maximumTime" 324 11 WRITE * 143569 "spec.jbb.TimerData.maximumTime" 497 1 READ *** *** AV-I --- 143553 "spec.jbb.TimerData.minimumTime" 471 1 READ * 143080 "spec.jbb.TimerData.minimumTime" 321 11 WRITE * 143558 "spec.jbb.TimerData.minimumTime" 479 1 READ *** *** AV-I --- 143548 "spec.jbb.TimerData.minimumTime" 463 1 READ * 143080 "spec.jbb.TimerData.minimumTime" 321 11 WRITE * 143563 "spec.jbb.TimerData.minimumTime" 487 1 READ *** *** AV-I --- 143554 "spec.jbb.TimerData.maximumTime" 473 1 READ * 143082 "spec.jbb.TimerData.maximumTime" 324 11 WRITE * 143559 "spec.jbb.TimerData.maximumTime" 481 1 READ *** *** AV-I --- 143543 "spec.jbb.TimerData.minimumTime" 455 1 READ * 143080 "spec.jbb.TimerData.minimumTime" 321 11 WRITE * 143563 "spec.jbb.TimerData.minimumTime" 487 1 READ *** *** AV-I --- 143543 "spec.jbb.TimerData.minimumTime" 455 1 READ * 143080 "spec.jbb.TimerData.minimumTime" 321 11 WRITE * 143558 "spec.jbb.TimerData.minimumTime" 479 1 READ *** *** AV-I --- 143558 "spec.jbb.TimerData.minimumTime" 479 1 READ * 143080 "spec.jbb.TimerData.minimumTime" 321 11 WRITE * 143563 "spec.jbb.TimerData.minimumTime" 487 1 READ *** *** AV-I --- 143548 "spec.jbb.TimerData.minimumTime" 463 1 READ * 143080 "spec.jbb.TimerData.minimumTime" 321 11 WRITE * 143558 "spec.jbb.TimerData.minimumTime" 479 1 READ *** *** AV-I --- 143549 "spec.jbb.TimerData.maximumTime" 465 1 READ * 143082 "spec.jbb.TimerData.maximumTime" 324 11 WRITE * 143554 "spec.jbb.TimerData.maximumTime" 473 1 READ *** *** AV-I --- 143553 "spec.jbb.TimerData.minimumTime" 471 1 READ * 143080 "spec.jbb.TimerData.minimumTime" 321 11 WRITE * 143563 "spec.jbb.TimerData.minimumTime" 487 1 READ *** *** AV-I --- 143559 "spec.jbb.TimerData.maximumTime" 481 1 READ * 143082 "spec.jbb.TimerData.maximumTime" 324 11 WRITE * 143564 "spec.jbb.TimerData.maximumTime" 489 1 READ *** *** AV-I --- 143554 "spec.jbb.TimerData.maximumTime" 473 1 READ * 143082 "spec.jbb.TimerData.maximumTime" 324 11 WRITE * 143564 "spec.jbb.TimerData.maximumTime" 489 1 READ *** *** AV-I --- 143544 "spec.jbb.TimerData.maximumTime" 457 1 READ * 143082 "spec.jbb.TimerData.maximumTime" 324 11 WRITE * 143564 "spec.jbb.TimerData.maximumTime" 489 1 READ *** *** AV-I --- 143549 "spec.jbb.TimerData.maximumTime" 465 1 READ * 143082 "spec.jbb.TimerData.maximumTime" 324 11 WRITE * 143564 "spec.jbb.TimerData.maximumTime" 489 1 READ *** *** AV-I --- 143544 "spec.jbb.TimerData.maximumTime" 457 1 READ * 143082 "spec.jbb.TimerData.maximumTime" 324 11 WRITE * 143559 "spec.jbb.TimerData.maximumTime" 481 1 READ *** *** AV-I --- 143544 "spec.jbb.TimerData.maximumTime" 457 1 READ * 143082 "spec.jbb.TimerData.maximumTime" 324 11 WRITE * 143554 "spec.jbb.TimerData.maximumTime" 473 1 READ *** *** AV-I --- 143549 "spec.jbb.TimerData.maximumTime" 465 1 READ * 143082 "spec.jbb.TimerData.maximumTime" 324 11 WRITE * 143559 "spec.jbb.TimerData.maximumTime" 481 1 READ *** ------------------------------------- Number of Threads: 4 Number of Shared Variables: 116 Number of Lock Nodes: 3238 Number of Message Nodes: 21 Number of Non-Method Entry/Exit Nodes: 143706 Number of Read/Write Nodes: 140447 Number of Total Nodes: 601248 Number of Races: 53 Number of Atomicity Violations: 31 Number of ASVs: 0