首页>
外国专利>
Automatic verification and synthesis for weak memory models
Automatic verification and synthesis for weak memory models
展开▼
机译:自动验证和综合弱存储模型
展开▼
页面导航
摘要
著录项
相似文献
摘要
Techniques are provided for automatic verification and inference of memory fences in concurrent programs that can bound the store buffers that are used to model relaxed memory models. A method is provided for determining whether a program employing a relaxed memory model satisfies a safety specification. An abstract memory model is obtained of the relaxed memory model. The abstract memory model represents concrete program states of the program as a finite number of abstract states. The safety specification is evaluated for the program on the abstract memory model having the finite number of abstract states. Fence positions at one or more locations can be determined to ensure that the safety specification is satisfied.
展开▼