• Developers:
    Caroline J. Trippel (Princeton)
    Publication ID:
    Publication Type:
    Software Description
    1 (17-May-2017)
    Received Date:
    Last Edit Date:
    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

Important Information for the SRC website. This site uses cookies to store information on your computer. By continuing to use our site, you consent to our cookies. If you are not happy with the use of these cookies, please review our Cookie Policy to learn how they can be disabled. By disabling cookies, some features of the site will not work.