Here are the two M-CMP benchmark protocols: inclusive and non-inclusive. Each benchmark includes the M-CMP protocol, and the set of abstract protocols after refinement. Also, here are the set of abstract protocols which are automatically generated: inclusive and noninclusive. These are the initial set of abstract protocols before refinement. The program which mechanizes the abstraction process is here. This tool was implemented by Michael Delisi, and the description of the tool is here.
Recently we add another multicore benchmark protocol which uses snoopy protocols inside a chip: snoop.

Home People Research Admissions Site Map