Skip to content

Verification of the Linearization Protocol proposed in: Scale-out CcNUMA: Exploiting Skew with Strongly Consistent Caching

Notifications You must be signed in to change notification settings

icsa-caps/Linearization-Protocol

 
 

Repository files navigation


To run the model checking of the Linearization Protocol:
1) Install CMurphi
2) Set path to Murphi in Makefile
3) $ make
4) $ ./VIW -m 128000

The original protocol implementation in the publication is not safe if a TS overflow occurs.
Given a sufficiently larger interger a TS overflow should never happen during the runtime of a system,
however, if for any reason the TS can only be an interger with few bits, a overflow safe version of the protocol is provided as well. 

About

Verification of the Linearization Protocol proposed in: Scale-out CcNUMA: Exploiting Skew with Strongly Consistent Caching

Resources

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published

Languages

  • C++ 68.3%
  • Objective-C 16.3%
  • Python 15.0%
  • Makefile 0.4%