| 主权项 |
1. A method for determining whether a program satisfies a safety specification, wherein said program employs a relaxed memory model, said method comprising:
obtaining an abstract memory model of said relaxed memory model, wherein said abstract memory model represents concrete program states of said program as a finite number of abstract states, wherein said relaxed memory model uses one or more store buffers and wherein said one or more store buffers are represented in said abstract memory model in a bounded way by maintaining order information between elements in a corresponding store buffer only up to a predefined bound and by handling elements in said corresponding store buffer beyond said predefined bound as an unordered set, wherein said abstract memory model preserves intra-process coherence by maintaining recency information per variable, wherein said recency information comprises an indication of how recently the respective variable was stored; determining one or more fence positions at one or more locations to ensure said safety specification is satisfied, wherein said one or more fence locations ensure that if a process pi performs a fence when its buffer for variable x is non-empty, a value of x visible to one or more additional processes immediately after the fence location, is a most recent value written by said process pi; and evaluating said safety specification for said program on said abstract memory model having said finite number of abstract states. |
