TriCheck

  • Developers:
    Caroline J. Trippel (Princeton)
    Publication ID:
    P090962
    Publication Type:
    Software Description
    Version/Date:
    1 (17-May-2017)
    Received Date:
    22-May-2017
    Last Edit Date:
    22-May-2017
    Research:
    2384.008 (University of Michigan)

Software Description

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.

4819 Emperor Blvd, Suite 300 Durham, NC 27703 Voice: (919) 941-9400 Fax: (919) 941-9450