Purpose and Function
TriCheck is the first tool capable of full stack memory consistency model verification, bridging HLL, compiler mappings, ISA, and microarchitecture. Overall correctness requires cooperation of the whole stack, and any changes to any component merit re-running TriCheck.
TriCheck is litmus test-based verification. TriCheck auto-generates all C11 permutations for a given litmus test in order to comprehensively analyze HLL ordering options, compiler mapping variations and ISA options. Like the other Check tools we have developed, TriCheck features graph-based happens-before analysis. Nodes are memory accesses & ordering primitives. Edges are event orders discerned via memory model relations. TriCheck is efficient top-to-bottom analysis that runs in second or minutes, which enables us to find real bugs.