کد مقاله کد نشریه سال انتشار مقاله انگلیسی نسخه تمام متن
429546 687597 2015 30 صفحه PDF دانلود رایگان
عنوان انگلیسی مقاله ISI
Locks: Picking key methods for a scalable quantitative analysis
ترجمه فارسی عنوان
قفل: انتخاب روش های کلیدی برای یک تجزیه و تحلیل کمی مقیاس پذیر یک؟
موضوعات مرتبط
مهندسی و علوم پایه مهندسی کامپیوتر نظریه محاسباتی و ریاضیات
چکیده انگلیسی


• 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.

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.

ناشر
Database: Elsevier - ScienceDirect (ساینس دایرکت)
Journal: Journal of Computer and System Sciences - Volume 81, Issue 1, February 2015, Pages 258–287
نویسندگان
, , , , , , , , ,