Abstract interpretation has been shown to be a promising technique for the thread-modular verification of concurrent programs. Central to this is the generation of interferences, in the form of rely-guarantee conditions, conforming to a user-chosen structure. In this work, we introduce one such structure called the conditional-writes domain, designed for programs where it suffices to establish only the conditions under which particular variables are written to by each thread. We formalise our analysis within a novel abstract interpretation framework that is highly modular and can be easily extended to capture other structures for rely-guarantee conditions. We formalise two versions of our approach and evaluate their implementations on a simple programming language.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

Generating Rely-Guarantee Conditions with the Conditional-Writes Domain

  • James Tobler,
  • Graeme Smith

摘要

Abstract interpretation has been shown to be a promising technique for the thread-modular verification of concurrent programs. Central to this is the generation of interferences, in the form of rely-guarantee conditions, conforming to a user-chosen structure. In this work, we introduce one such structure called the conditional-writes domain, designed for programs where it suffices to establish only the conditions under which particular variables are written to by each thread. We formalise our analysis within a novel abstract interpretation framework that is highly modular and can be easily extended to capture other structures for rely-guarantee conditions. We formalise two versions of our approach and evaluate their implementations on a simple programming language.