VeriLin: A Linearizability Checker for Large-Scale Concurrent Objects

Theoretical Aspects of Software Engineering(2023)

引用 0|浏览27
暂无评分
摘要
Linearizability is an important correctness criterion for concurrent objects, and there have been several existing tools for checking linearizability. However, due to the inherent exponential complexity of the problem, existing tools have difficulty scaling up to large, industrial-sized concurrent objects. In this paper, we introduce VeriLin, a new linearizability checker that incorporates a more general checking algorithm as well as associated testing strategies, that allow it to continue to be effective for large-scale concurrent objects and long histories. For evaluation, we apply VeriLin to checking linearizability of student implementations of a train ticketing system, as well as the task management and scheduling module of a proprietary multicore operating system.
更多
查看译文
关键词
linearizability checker,large-scale
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要