Locks: Picking key methods for a scalable quantitative analysis
Locks: Picking key methods for a scalable quantitative analysis
复制标题
Locks：选择关键方法进行可扩展的定量分析
DOI：
10.1016/j.jcss.2014.06.004
复制
发表时间：
2015
期刊：
影响因子：
--
通讯作者：
Marcus Völp
中科院分区：
文献类型：
--
作者：
Christel Baier;Marcus Daum;Benjamin Engel;Hermann Härtig;Joachim Klein;Sascha Klüppelholz;Steffen Märcker;Hendrik Tews;Marcus Völp
底层操作系统（OS）代码的功能正确性是不可或缺的要求。然而，许多应用还依赖于定量方面，例如速度、能源效率、关于错误的弹性和其他成本因素。我们报告我们的经验，应用概率模型检测技术分析定量的低级别操作系统代码的长期行为。我们的方法，说明在一个案例研究分析一个简单的测试和测试和设置（TTS）自旋锁协议，结合基于测量的模拟与概率模型检查，以获得高层次的模型，现实系统的性能，并调整模型来预测未来的系统行为。我们报告我们如何获得了一个近乎完美的匹配的分析结果和测量，以及我们如何解决状态爆炸问题，以获得大量的过程中的测量不再可行的模型检查结果。这些结果为我们提供了有价值的见解，在锁负载，平均旋转时间和其他性能指标之间的微妙的相互作用。
Functional correctness of low-level operating-system (OS) code is an indispensable requirement. However, many applications rely also on quantitative aspects such as speed, energy efficiency, resilience with regards to errors and other cost factors. We report on our experiences of applying probabilistic model-checking techniques for analysing the quantitative long-run behaviour of low-level OS-code. Our approach, illustrated in a case study analysing a simple test-and-test-and-set (TTS) spinlock protocol, combines measure-based simulation with probabilistic model-checking to obtain high-level models of the performance of realistic systems and to tune the models to predict future system behaviour. We report how we obtained a nearly perfect match of analytic results and measurements and how we tackled the state-explosion problem to obtain model-checking results for a large number of processes where measurements are no longer feasible. These results gave us valuable insights in the delicate interplay between lock load, average spinning times and other performance measures.
登录
查看更多内容
主要对称：操作系统代码概率模型检查的可扩展性结果
影响因子：
1
作者：
C. Baier;Marcus Daum;Benjamin Engel;Hermann Härtig;Joachim Klein;Sascha Klüppelholz;Steffen Märcker;H. Tews;M. Völp
通讯作者：
M. Völp
DOI：
--
发表时间：
2011
期刊：
International Conference on Computer Aided Verification
影响因子：
--
作者：
Pavol Cerný;K. Chatterjee;T. Henzinger;Arjun Radhakrishna;Rohit Singh
通讯作者：
Rohit Singh
保证质量的调度——利用随机行为提高资源利用率
DOI：
10.1109/real.2001.990603
发表时间：
2001
期刊：
Proceedings 22nd IEEE Real-Time Systems Symposium (RTSS 2001) (Cat. No.01PR1420)
影响因子：
--
作者：
Claude;Lars Reuther;Jork Wolter;Hermann Härtig;Jork Löser;S. Schönberg
通讯作者：
S. Schönberg
基于CADP的共享内存互斥协议研究
DOI：
10.1007/978-3-642-15898-8_12
发表时间：
2010
期刊：
ACM Trans. Storage
影响因子：
--
作者：
Radu Mateescu;Wendelin Serwe
通讯作者：
Wendelin Serwe
普遍系统验证背景下的现实最坏情况执行时间分析
DOI：
10.1007/978-3-540-71322-7_3
发表时间：
2006
期刊：
ACM Trans. Storage
影响因子：
--
作者：
Steffen Knapp;W. Paul
通讯作者：
W. Paul