发表机构
Technical University of Munich; CISPA Helmholtz-Zentrum; National University of Singapore（慕尼黑工业大学; CISPA亥姆霍兹信息与安全中心; 新加坡国立大学）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
该研究扩展digest框架以处理静态数据竞争检测中被忽略的并发结构，引入线程屏障、pthread_once等机制，通过litmus测试评估并对比现有工具，发现其缺乏相关支持，提升了数据竞争检测精度。
AI 中文摘要
维护线程执行历史的抽象可提升静态分析中数据竞争检测的精度。本文将digest框架扩展至处理静态竞争检测中被忽略的并发结构与同步机制，引入常用线程屏障及pthread_once的处理机制（pthread_once用于确保某操作仅执行一次），还实例化该框架以抽象祖先线程持有的锁集。本文提出一组litmus测试评估针对这些特性的分析，并将实现与最先进工具对比，发现现有工具缺乏相关支持。
英文摘要
Maintaining an abstraction of the execution history of threads can improve the precision of data race detection in static analysis. Here, we extend the digest framework to handle concurrency constructs and synchronization mechanisms that have been ignored in static race detection. We introduce mechanisms for the commonly used thread barriers, as well as pthread_once, which allows to ensure that an action is executed only once. We also instantiate the framework with an abstraction of locksets held by ancestor threads. We propose a suite of litmus tests to evaluate analyses for these features and compare our implementation to state-of-the-art tools, finding that they lack support.
Comments49 pages, 12 figures, 6 tables
