Program executions under relaxed memory model (rmm) semantics are significantly more difficult to analyze; the rmm semantics result in out of order execution of program events leading to an explosion of state-space. Dynamic partial order reduction (DPOR) is a powerful technique to address such a state-space explosion and has been used to verify programs under rmm such as TSO, PSO, and POWER. Central to such DPOR techniques is the notion of trace-equivalence, which is computed based on the independence relation among program events. We propose a coarser notion of rmm-aware trace equivalence called observational equivalence (OE). Two program behaviors are observationally equivalent if every read event reads the same value in both the behaviors. We propose a notion of observational independence (OI) and provide an algorithmic construction to compute trace equivalence (modulo OI) efficiently. We also demonstrate the effectiveness of DPOR with OE on threaded C/C++ programs by first providing an elaborate happensbefore (hb) relation for capturing the C/C++ concurrency semantics. We implement the presented technique in a runtime model checker called Drista. Our experiments reflect that (i) when compared to existing nonOE techniques, we achieve significant savings in the number of traces explored under OE, and (ii) our treatment of C/C++ concurrency is more extensive than the existing state-of-the-art techniques.


翻译:在宽松的记忆模型(rmm)语义学下,程序执行过程在宽松的记忆模型(rmm)语义学下,分析起来要困难得多;语义学导致程序事件执行的秩序导致州空间爆炸的爆炸。动态部分排序(DPOR)是处理这种州空间爆炸的有力技术,并被用于核查程序,如TSO、PSO和POWER。这种DPOR技术的核心是追踪等同概念,它是根据方案事件的独立性关系计算的。我们提出了一种粗略的Rmm-aware追踪等同概念,称为观测等同(OE)。如果每个阅读事件在两种行为中都有同样的价值,则两种程序行为在观察上是等同的。我们提出了观察独立(OI)的概念,并提供了一种算法结构构造,以有效地计算等等同(Modulo OI OI) 。我们还展示了DPOR和OE 在线性C/C++程序上与OE 的等同概念的有效性,首先提供了详细的预想(h) 与捕捉捉到C/C+conmantictict(h) rodual Te) 相比,在运行中我们现有的货币技术中,我们现有的C-C-C-tratitutionroticreal 是在进行重大的实验中,我们现有的技术,我们在进行重大的C-trac-tatic-tratical 。我们进行重大的实验,我们现有的技术,我们在进行重大的实验。我们现有的技术,我们在进行重大的C-toal-traal-toal-toal-toal-tratratratatic-tra 。

0
下载
关闭预览

相关内容

不可错过!700+ppt《因果推理》课程!杜克大学Fan Li教程
专知会员服务
69+阅读 · 2022年7月11日
不可错过!《机器学习100讲》课程,UBC Mark Schmidt讲授
专知会员服务
73+阅读 · 2022年6月28日
专知会员服务
25+阅读 · 2021年4月2日
专知会员服务
159+阅读 · 2020年1月16日
Keras François Chollet 《Deep Learning with Python 》, 386页pdf
专知会员服务
151+阅读 · 2019年10月12日
机器学习入门的经验与建议
专知会员服务
92+阅读 · 2019年10月10日
【哈佛大学商学院课程Fall 2019】机器学习可解释性
专知会员服务
103+阅读 · 2019年10月9日
VCIP 2022 Call for Special Session Proposals
CCF多媒体专委会
1+阅读 · 2022年4月1日
AIART 2022 Call for Papers
CCF多媒体专委会
1+阅读 · 2022年2月13日
【ICIG2021】Check out the hot new trailer of ICIG2021 Symposium8
中国图象图形学学会CSIG
0+阅读 · 2021年11月16日
【ICIG2021】Check out the hot new trailer of ICIG2021 Symposium6
中国图象图形学学会CSIG
2+阅读 · 2021年11月12日
【ICIG2021】Check out the hot new trailer of ICIG2021 Symposium4
中国图象图形学学会CSIG
0+阅读 · 2021年11月10日
【ICIG2021】Check out the hot new trailer of ICIG2021 Symposium2
中国图象图形学学会CSIG
0+阅读 · 2021年11月8日
【ICIG2021】Latest News & Announcements of the Plenary Talk1
中国图象图形学学会CSIG
0+阅读 · 2021年11月1日
【ICIG2021】Latest News & Announcements of the Industry Talk2
中国图象图形学学会CSIG
0+阅读 · 2021年7月29日
Hierarchically Structured Meta-learning
CreateAMind
26+阅读 · 2019年5月22日
A Technical Overview of AI & ML in 2018 & Trends for 2019
待字闺中
16+阅读 · 2018年12月24日
国家自然科学基金
1+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2013年12月31日
国家自然科学基金
0+阅读 · 2013年12月31日
国家自然科学基金
1+阅读 · 2013年12月31日
国家自然科学基金
1+阅读 · 2012年12月31日
国家自然科学基金
0+阅读 · 2012年8月18日
国家自然科学基金
0+阅读 · 2009年12月31日
国家自然科学基金
0+阅读 · 2009年12月31日
国家自然科学基金
0+阅读 · 2008年12月31日
Arxiv
0+阅读 · 2022年9月28日
Arxiv
0+阅读 · 2022年9月27日
Arxiv
110+阅读 · 2020年2月5日
VIP会员
相关VIP内容
相关资讯
VCIP 2022 Call for Special Session Proposals
CCF多媒体专委会
1+阅读 · 2022年4月1日
AIART 2022 Call for Papers
CCF多媒体专委会
1+阅读 · 2022年2月13日
【ICIG2021】Check out the hot new trailer of ICIG2021 Symposium8
中国图象图形学学会CSIG
0+阅读 · 2021年11月16日
【ICIG2021】Check out the hot new trailer of ICIG2021 Symposium6
中国图象图形学学会CSIG
2+阅读 · 2021年11月12日
【ICIG2021】Check out the hot new trailer of ICIG2021 Symposium4
中国图象图形学学会CSIG
0+阅读 · 2021年11月10日
【ICIG2021】Check out the hot new trailer of ICIG2021 Symposium2
中国图象图形学学会CSIG
0+阅读 · 2021年11月8日
【ICIG2021】Latest News & Announcements of the Plenary Talk1
中国图象图形学学会CSIG
0+阅读 · 2021年11月1日
【ICIG2021】Latest News & Announcements of the Industry Talk2
中国图象图形学学会CSIG
0+阅读 · 2021年7月29日
Hierarchically Structured Meta-learning
CreateAMind
26+阅读 · 2019年5月22日
A Technical Overview of AI & ML in 2018 & Trends for 2019
待字闺中
16+阅读 · 2018年12月24日
相关基金
国家自然科学基金
1+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2013年12月31日
国家自然科学基金
0+阅读 · 2013年12月31日
国家自然科学基金
1+阅读 · 2013年12月31日
国家自然科学基金
1+阅读 · 2012年12月31日
国家自然科学基金
0+阅读 · 2012年8月18日
国家自然科学基金
0+阅读 · 2009年12月31日
国家自然科学基金
0+阅读 · 2009年12月31日
国家自然科学基金
0+阅读 · 2008年12月31日
Top
微信扫码咨询专知VIP会员