Atomicity is a correctness criterion to reason about multithreaded programs in program analysis and debugging. Atomicity violations, in general, account for the majority of concurrency bugs in these programs. When an execution does not produce a dynamic instance of an atomic code region, called transaction, to execute serially without interfering with other transactions, a transactional atomicity violation occurs.

On the one hand, existing dynamic graph-based atomicity checkers explicitly build a transactional happens-before graph along a given trace and detect non-serializable traces through locating cycles in the graph. These techniques produce either false negatives or false positives in reporting transactional atomicity violations. On the other hand, existing dynamic vector-clock-based checkers either detect all transactional atomicity violations or all non-serializable traces, but not both.

This thesis presents a comprehensive framework to address these challenges.

The first contribution of this thesis is to formulate a novel, sound, and complete dynamic checker to detect transactional atomicity violations and non-serializable traces. To detect transactional atomicity violations, the checker streamlines the detection of existing work. To detect non-serializable traces, it maintains the reversal frontier transactional happens-before relations through its transactional vector clocks and novel timestamp propagation approach, which captures transaction-level happens-before relations that cannot be transmitted by event-level happens-before relations, without traversing other entities. The empirical results confirmed that the checker efficiently detected transactional atomicity violations and non-serializable traces without false positives, and all violations on transactions and traces reported by existing work were reported by it.

The second contribution of this thesis is to propose a novel and sound checker to detect transactional atomicity violations each with a witness. It selectively encodes the increasing transactional happens-before relations in transactional happens before tree instances sufficient for determining the inference on transitivity of transactional happens-before relations with a novel update mechanism. It further precisely locates witnesses leading to such violations. The experiment results showed that the checker detected all transactional atomicity violations and localized a witness for each violation.

All above-mentioned checkers cannot detect transactional atomicity violations that may appear in other possible executions of the given traces but not in these traces due to the presence of some incidental happens-before dependences. These dependences may reverse their direction in other possible executions of the traces.

The third contribution of this thesis is to propose a novel and sound checker to detect predictive transactional atomicity violations. It detects commutable happens-before dependences and tracks the increasing transactional happens-before dependences through its novel mechanism. The experiment results showed that it detected predictive transactional atomicity violations difficult to be detected by existing checkers without checking more traces.

In summary, this thesis presents a novel framework to detect in-trace and predictive transactional atomicity violations as well as non-serializable traces. First, it presents the first work in sound and complete detection of both transactional atomicity violations and non-serializable traces. It also presents the first work to localize a witness for each transactional atomicity violation without explicit graph construction and soundly detect predictive transactional atomicity violations that are not observed in given traces.