Locks: Picking key methods for a scalable quantitative analysis

Christel BaierChristel Baier, Marcus DaumMarcus Daum, Benjamin EngelBenjamin Engel, Hermann HärtigHermann Härtig, Joachim KleinJoachim Klein, Sascha KlüppelholzSascha Klüppelholz, Steffen MärckerSteffen Märcker, Hendrik TewsHendrik Tews, Marcus VölpMarcus Völp

DOI Link

Christel Baier, Marcus Daum, Benjamin Engel, Hermann Härtig, Joachim Klein, Sascha Klüppelholz, Steffen Märcker, Hendrik Tews, Marcus Völp
Locks: Picking key methods for a scalable quantitative analysis
Journal of Computer and System Sciences, 81(1):258--287, 2015

Details
Bibtex

KurzfassungAbstract
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.
Forschungsgruppe:Research Group: Verifikation und formale quantitative Analyse„Verifikation und formale quantitative Analyse“ befindet sich nicht in der Liste (Computational Logic, Automatentheorie, Wissensverarbeitung, Knowledge-Based Systems, Knowledge Systems, Wissensbasierte Systeme, Logische Programmierung und Argumentation, Algebra und Diskrete Strukturen, Knowledge-aware Artificial Intelligence, Algebraische und logische Grundlagen der Informatik) zulässiger Werte für das Attribut „Forschungsgruppe“.Algebraic and Logical Foundations of Computer Science

@article{BDEHKKMTV2015,
  author    = {Christel Baier and Marcus Daum and Benjamin Engel and Hermann
               H{\"{a}}rtig and Joachim Klein and Sascha Kl{\"{u}}ppelholz and
               Steffen M{\"{a}}rcker and Hendrik Tews and Marcus V{\"{o}}lp},
  title     = {Locks: Picking key methods for a scalable quantitative analysis},
  journal   = {Journal of Computer and System Sciences},
  volume    = {81},
  number    = {1},
  publisher = {Elsevier},
  year      = {2015},
  pages     = {258--287},
  doi       = {10.1016/j.jcss.2014.06.004}
}