Locks: Picking key methods for a scalable quantitative analysis

作者：

Highlights：

• Probabilistic model checking for quantitative analysis of low-level OS primitives.

• Combine measure-based analysis with formal modelling, spinlock protocol case study.

• Report on challenges and methods, tackling state-explosion problem.

摘要

•Probabilistic model checking for quantitative analysis of low-level OS primitives.•Combine measure-based analysis with formal modelling, spinlock protocol case study.•Report on challenges and methods, tackling state-explosion problem.

论文关键词：Probabilistic model checking,Measure-based quantitative analysis,Low-level operating system code,Test-and-test-and-set spinlock,Conditional long-run probabilities,Quantile-based queries,Symmetry reduction

论文评审过程：Received 24 May 2013, Revised 13 January 2014, Accepted 18 May 2014, Available online 23 July 2014.

论文官网地址：https://doi.org/10.1016/j.jcss.2014.06.004