-
The Probability Spaces of QuickSort
Authors:
George Nadareishvili,
Jonas Oberhauser,
Wolfgang J. Paul
Abstract:
QuickSort and the analysis of its expected run time was presented 1962 in a classical paper by C.A.R Hoare. There the run time analysis hinges on a by now well known recurrence equation for the expected run time, which in turn was justified by referring to ``the law of conditional expectations''. A probability space for the runs of the algorithms was not constructed. Subsequent textbooks treated t…
▽ More
QuickSort and the analysis of its expected run time was presented 1962 in a classical paper by C.A.R Hoare. There the run time analysis hinges on a by now well known recurrence equation for the expected run time, which in turn was justified by referring to ``the law of conditional expectations''. A probability space for the runs of the algorithms was not constructed. Subsequent textbooks treated the recurrence relation as self evident and present it until this day without proof. Here we give an inductive definition of the probability space for the runs of randomized QuickSort and subsequently derive the recurrence equation with a not completely trivial proof.
△ Less
Submitted 19 June, 2025; v1 submitted 5 April, 2025;
originally announced April 2025.
-
VSync: Push-Button Verification and Optimization for Synchronization Primitives on Weak Memory Models (Technical Report)
Authors:
Jonas Oberhauser,
Rafael Lourenco de Lima Chehab,
Diogo Behrens,
Ming Fu,
Antonio Paolillo,
Lilith Oberhauser,
Koustubha Bhat,
Yuzhong Wen,
Haibo Chen,
Jaeho Kim,
Viktor Vafeiadis
Abstract:
This technical report contains material accompanying our work with same title published at ASPLOS'21. We start in Sec. 1 with a detailed presentation of the core innovation of this work, Await Model Checking (AMC). The correctness proofs of AMC can be found in Sec. 2. Next, we discuss three study cases in Sec. 3, presenting bugs found and challenges encountered when applying VSync to existing code…
▽ More
This technical report contains material accompanying our work with same title published at ASPLOS'21. We start in Sec. 1 with a detailed presentation of the core innovation of this work, Await Model Checking (AMC). The correctness proofs of AMC can be found in Sec. 2. Next, we discuss three study cases in Sec. 3, presenting bugs found and challenges encountered when applying VSync to existing code bases. Finally, in Sec. 4 we describe the setup details of our evaluation and report further experimental results.
△ Less
Submitted 12 February, 2021;
originally announced February 2021.
-
Making Weak Memory Models Fair
Authors:
Ori Lahav,
Egor Namakonov,
Jonas Oberhauser,
Anton Podkopaev,
Viktor Vafeiadis
Abstract:
Liveness properties, such as termination, of even the simplest shared-memory concurrent programs under sequential consistency typically require some fairness assumptions about the scheduler. Under weak memory models, we observe that the standard notions of thread fairness are insufficient, and an additional fairness property, which we call memory fairness, is needed. In this paper, we propose a un…
▽ More
Liveness properties, such as termination, of even the simplest shared-memory concurrent programs under sequential consistency typically require some fairness assumptions about the scheduler. Under weak memory models, we observe that the standard notions of thread fairness are insufficient, and an additional fairness property, which we call memory fairness, is needed. In this paper, we propose a uniform definition for memory fairness that can be integrated into any declarative memory model enforcing acyclicity of the union of the program order and the reads-from relation. For the well-known models, SC, x86-TSO, RA, and StrongCOH, that have equivalent operational and declarative presentations, we show that our declarative memory fairness condition is equivalent to an intuitive model-specific operational notion of memory fairness, which requires the memory system to fairly execute its internal propagation steps. Our fairness condition preserves the correctness of local transformations and the compilation scheme from RC11 to x86-TSO, and also enables the first formal proofs of termination of mutual exclusion lock implementations under declarative weak memory models.
△ Less
Submitted 9 September, 2021; v1 submitted 2 December, 2020;
originally announced December 2020.
