Effective abstractions for verification under relaxed memory models

详细信息    查看全文

• 作者：Andrei Dan^a ; ^{andrei.dan@inf.ethz.ch} ; Yuri Meshman^b ; ^{yurime@cs.technion.ac.il} ; Martin Vechev^a ; ^{martin.vechev@inf.ethz.ch} ; Eran Yahav^b ; ^{yahave@cs.technion.ac.il}
• 关键词：Abstract interpretation ; Relaxed memory models
• 刊名：Computer Languages, Systems & Structures
• 出版年：2017
• 出版时间：January 2017
• 年：2017
• 卷：47
• 期：part_P1
• 页码：62-76
• 全文大小：980 K
• 卷排序：47

文摘

A new abstraction of the ×86 TSO and PSO memory models is proposed. The abstraction significantly improves the precision and scalability of the program analysis. Automatically verify algorithms with fewer fences, faster and with lower memory consumption.