19 Search Results for "Hendler, Danny"

Document
DOI: 10.4230/LIPIcs.OPODIS.2025.17
Recoverable Lock-Free Locks

Authors: Hagit Attiya, Panagiota Fatourou, Eleftherios Kosmas, and Yuanhao Wei

Published in: LIPIcs, Volume 361, 29th International Conference on Principles of Distributed Systems (OPODIS 2025)

Abstract
This paper presents the first transformation that introduces both lock-freedom and recoverability. Our transformation starts with a lock-based implementation, and provides a recoverable, lock-free substitution to lock acquire and lock release operations. The transformation supports nested locks for generality and ensures recoverability without jeopardising the correctness of the lock-based implementation it is applied on.
Cite as

Hagit Attiya, Panagiota Fatourou, Eleftherios Kosmas, and Yuanhao Wei. Recoverable Lock-Free Locks. In 29th International Conference on Principles of Distributed Systems (OPODIS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 361, pp. 17:1-17:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{attiya_et_al:LIPIcs.OPODIS.2025.17,
  author =	{Attiya, Hagit and Fatourou, Panagiota and Kosmas, Eleftherios and Wei, Yuanhao},
  title =	{{Recoverable Lock-Free Locks}},
  booktitle =	{29th International Conference on Principles of Distributed Systems (OPODIS 2025)},
  pages =	{17:1--17:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-409-3},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{361},
  editor =	{Arusoaie, Andrei and Onica, Emanuel and Spear, Michael and Tucci-Piergiovanni, Sara},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.OPODIS.2025.17},
  URN =		{urn:nbn:de:0030-drops-251905},
  doi =		{10.4230/LIPIcs.OPODIS.2025.17},
  annote =	{Keywords: recoverable computing, NVM, lock, lock-freedom}
}
Document
DOI: 10.4230/LIPIcs.OPODIS.2025.33
Resolving Conflicts with Grace: Dynamically Concurrent Universality

Authors: Petr Kuznetsov and Nathan Josia Schrodt

Published in: LIPIcs, Volume 361, 29th International Conference on Principles of Distributed Systems (OPODIS 2025)

Abstract
Synchronization is the major obstacle to scalability in distributed computing. Concurrent operations on the shared data engage in synchronization when they encounter a conflict, i.e., their effects depend on the order in which they are applied. Ideally, one would like to detect conflicts in a dynamic manner, i.e., adjusting to the current system state. Indeed, it is very common that two concurrent operations conflict only in some rarely occurring states. In this paper, we define the notion of dynamic concurrency: an operation employs strong synchronization primitives only if it has to arbitrate with concurrent operations, given the current system state. We then present a dynamically concurrent universal construction.
Cite as

Petr Kuznetsov and Nathan Josia Schrodt. Resolving Conflicts with Grace: Dynamically Concurrent Universality. In 29th International Conference on Principles of Distributed Systems (OPODIS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 361, pp. 33:1-33:29, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{kuznetsov_et_al:LIPIcs.OPODIS.2025.33,
  author =	{Kuznetsov, Petr and Schrodt, Nathan Josia},
  title =	{{Resolving Conflicts with Grace: Dynamically Concurrent Universality}},
  booktitle =	{29th International Conference on Principles of Distributed Systems (OPODIS 2025)},
  pages =	{33:1--33:29},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-409-3},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{361},
  editor =	{Arusoaie, Andrei and Onica, Emanuel and Spear, Michael and Tucci-Piergiovanni, Sara},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.OPODIS.2025.33},
  URN =		{urn:nbn:de:0030-drops-252068},
  doi =		{10.4230/LIPIcs.OPODIS.2025.33},
  annote =	{Keywords: Universal Construction, Consensus, Dynamic Concurrency}
}
Document
Research
DOI: 10.4230/TGDK.3.3.4
Mining Inter-Document Argument Structures in Scientific Papers for an Argument Web

Authors: Florian Ruosch, Cristina Sarasua, and Abraham Bernstein

Published in: TGDK, Volume 3, Issue 3 (2025). Transactions on Graph Data and Knowledge, Volume 3, Issue 3

Abstract
In Argument Mining, predicting argumentative relations between texts (or spans) remains one of the most challenging aspects, even more so in the cross-document setting. This paper makes three key contributions to advance research in this domain. We first extend an existing dataset, the Sci-Arg corpus, by annotating it with explicit inter-document argumentative relations, thereby allowing arguments to be distributed over several documents forming an Argument Web; these new annotations are published using Semantic Web technologies (RDF, OWL). Second, we explore and evaluate three automated approaches for predicting these inter-document argumentative relations, establishing critical baselines on the new dataset. We find that a simple classifier based on discourse indicators with access to context outperforms neural methods. Third, we conduct a comparative analysis of these approaches for both intra- and inter-document settings, identifying statistically significant differences in results that indicate the necessity of distinguishing between these two scenarios. Our findings highlight significant challenges in this complex domain and open crucial avenues for future research on the Argument Web of Science, particularly for those interested in leveraging Semantic Web technologies and knowledge graphs to understand scholarly discourse. With this, we provide the first stepping stones in the form of a benchmark dataset, three baseline methods, and an initial analysis for a systematic exploration of this field relevant to the Web of Data and Science.
Cite as

Florian Ruosch, Cristina Sarasua, and Abraham Bernstein. Mining Inter-Document Argument Structures in Scientific Papers for an Argument Web. In Transactions on Graph Data and Knowledge (TGDK), Volume 3, Issue 3, pp. 4:1-4:33, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@Article{ruosch_et_al:TGDK.3.3.4,
  author =	{Ruosch, Florian and Sarasua, Cristina and Bernstein, Abraham},
  title =	{{Mining Inter-Document Argument Structures in Scientific Papers for an Argument Web}},
  journal =	{Transactions on Graph Data and Knowledge},
  pages =	{4:1--4:33},
  ISSN =	{2942-7517},
  year =	{2025},
  volume =	{3},
  number =	{3},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/TGDK.3.3.4},
  URN =		{urn:nbn:de:0030-drops-252159},
  doi =		{10.4230/TGDK.3.3.4},
  annote =	{Keywords: Argument Mining, Large Language Models, Knowledge Graphs, Link Prediction}
}
Document
DOI: 10.4230/LIPIcs.DISC.2025.3
An Almost-Logarithmic Lower Bound for Leader Election with Bounded Value Contention

Authors: Dan Alistarh, Faith Ellen, and Alexander Fedorov

Published in: LIPIcs, Volume 356, 39th International Symposium on Distributed Computing (DISC 2025)

Abstract
We investigate the step complexity of the Leader Election problem (and implementing the corresponding test-and-set object) in asynchronous shared memory, where processes communicate through registers supporting atomic read and write and must coordinate so that a single process becomes the leader. Determining tight step complexity bounds for solving this problem is one of the key open problems in the theory of shared memory distributed computing. The best known algorithm is a randomized tournament-tree, which has worst-case expected step complexity O(log N) for N processes. There are provably no deterministic wait-free algorithms, and only restricted lower bounds are known for obstruction-free and randomized wait-free algorithms. We introduce a new lower bound that establishes an Ω((log N)/(log log N + log Q)) step complexity for any obstruction-free Leader Election algorithm, where N is the number of processes, and 2 ≤ Q ≤ N is a bound on the value contention, which we define as the maximum number of different values that processes can be simultaneously poised to write to the same register in any execution of the algorithm. Our result is strictly stronger than previous bounds based on write contention. In particular, it implies new lower bounds on step complexity that depend on register size.
Cite as

Dan Alistarh, Faith Ellen, and Alexander Fedorov. An Almost-Logarithmic Lower Bound for Leader Election with Bounded Value Contention. In 39th International Symposium on Distributed Computing (DISC 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 356, pp. 3:1-3:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{alistarh_et_al:LIPIcs.DISC.2025.3,
  author =	{Alistarh, Dan and Ellen, Faith and Fedorov, Alexander},
  title =	{{An Almost-Logarithmic Lower Bound for Leader Election with Bounded Value Contention}},
  booktitle =	{39th International Symposium on Distributed Computing (DISC 2025)},
  pages =	{3:1--3:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-402-4},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{356},
  editor =	{Kowalski, Dariusz R.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.DISC.2025.3},
  URN =		{urn:nbn:de:0030-drops-248204},
  doi =		{10.4230/LIPIcs.DISC.2025.3},
  annote =	{Keywords: Leader Election, Test-and-Set, Shared Memory, Lower Bounds}
}
Document
DOI: 10.4230/LIPIcs.DISC.2025.35
PIPQ: Strict Insert-Optimized Concurrent Priority Queue

Authors: Olivia Grimes, Ahmed Hassan, Panagiota Fatourou, and Roberto Palmieri

Published in: LIPIcs, Volume 356, 39th International Symposium on Distributed Computing (DISC 2025)

Abstract
This paper presents PIPQ, a strict and linearizable concurrent priority queue whose design differs from existing solutions in literature because it focuses on enabling parallelism of insert operations as opposed to accelerating delete-min operations, as traditionally done. In a nutshell, PIPQ’s structure includes two levels: the worker level and the leader level. The worker level provides per-thread data structures enabling fast and parallel insertions. The leader level contains the highest priority elements in the priority queue and can thus serve delete-min operations. Our evaluation, which includes an exploration of different data access patterns, operation mixes, runtime settings, and an integration into a graph-based application, shows that PIPQ outperforms competitors in a variety of cases, especially with insert-dominant workloads.
Cite as

Olivia Grimes, Ahmed Hassan, Panagiota Fatourou, and Roberto Palmieri. PIPQ: Strict Insert-Optimized Concurrent Priority Queue. In 39th International Symposium on Distributed Computing (DISC 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 356, pp. 35:1-35:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{grimes_et_al:LIPIcs.DISC.2025.35,
  author =	{Grimes, Olivia and Hassan, Ahmed and Fatourou, Panagiota and Palmieri, Roberto},
  title =	{{PIPQ: Strict Insert-Optimized Concurrent Priority Queue}},
  booktitle =	{39th International Symposium on Distributed Computing (DISC 2025)},
  pages =	{35:1--35:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-402-4},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{356},
  editor =	{Kowalski, Dariusz R.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.DISC.2025.35},
  URN =		{urn:nbn:de:0030-drops-248525},
  doi =		{10.4230/LIPIcs.DISC.2025.35},
  annote =	{Keywords: Priority Queue, Concurrent Data Structures, Synchronization}
}
Document
DOI: 10.4230/LIPIcs.DISC.2025.29
Strong Linearizability Without Compare&Swap: The Case of Bags

Authors: Faith Ellen and Gal Sela

Published in: LIPIcs, Volume 356, 39th International Symposium on Distributed Computing (DISC 2025)

Abstract
Because strongly-linearizable objects provide stronger guarantees than linearizability, they serve as valuable building blocks for the design of concurrent data structures. Yet, many objects that have linearizable implementations from base objects weaker than compare&swap objects do not have strongly-linearizable implementations from the same base objects. We focus on one such object: the bag, a multiset from which processes can take unspecified elements. We present the first lock-free, strongly-linearizable implementation of a bag from interfering objects (specifically, registers and test&set objects). This may be surprising, since there are provably no such implementations of stacks or queues. Since a bag can contain arbitrarily many elements, an unbounded amount of space must be used to implement it. Hence, it makes sense to also consider a bag with a bound on its capacity. However, like stacks and queues, a bag with capacity b shared by more than 2b processes has no lock-free, strongly-linearizable implementation from interfering objects. If we further restrict a bounded bag so that only one process can insert into it, we are able to obtain a lock-free, strongly-linearizable implementation from O(b+n) interfering objects, where n is the number of processes. Our goal is to understand the circumstances under which strongly-linearizable implementations of bags exist and, more generally, to understand the power of interfering objects.
Cite as

Faith Ellen and Gal Sela. Strong Linearizability Without Compare&Swap: The Case of Bags. In 39th International Symposium on Distributed Computing (DISC 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 356, pp. 29:1-29:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{ellen_et_al:LIPIcs.DISC.2025.29,
  author =	{Ellen, Faith and Sela, Gal},
  title =	{{Strong Linearizability Without Compare\&Swap: The Case of Bags}},
  booktitle =	{39th International Symposium on Distributed Computing (DISC 2025)},
  pages =	{29:1--29:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-402-4},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{356},
  editor =	{Kowalski, Dariusz R.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.DISC.2025.29},
  URN =		{urn:nbn:de:0030-drops-248464},
  doi =		{10.4230/LIPIcs.DISC.2025.29},
  annote =	{Keywords: Strong-Linearizability, Bag, Concurrent Data Structures, Wait-Freedom, Lock-Freedom}
}
Document
Brief Announcement
DOI: 10.4230/LIPIcs.DISC.2025.55
Brief Announcement: Concurrent Double-Ended Priority Queues

Authors: Panagiota Fatourou, Eric Ruppert, and Ioannis Xiradakis

Published in: LIPIcs, Volume 356, 39th International Symposium on Distributed Computing (DISC 2025)

Abstract
This work provides the first concurrent implementation of a double-ended priority queue (DEPQ). We describe a general way to add an ExtractMax operation to any concurrent priority queue that already supports Insert and ExtractMin.
Cite as

Panagiota Fatourou, Eric Ruppert, and Ioannis Xiradakis. Brief Announcement: Concurrent Double-Ended Priority Queues. In 39th International Symposium on Distributed Computing (DISC 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 356, pp. 55:1-55:7, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{fatourou_et_al:LIPIcs.DISC.2025.55,
  author =	{Fatourou, Panagiota and Ruppert, Eric and Xiradakis, Ioannis},
  title =	{{Brief Announcement: Concurrent Double-Ended Priority Queues}},
  booktitle =	{39th International Symposium on Distributed Computing (DISC 2025)},
  pages =	{55:1--55:7},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-402-4},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{356},
  editor =	{Kowalski, Dariusz R.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.DISC.2025.55},
  URN =		{urn:nbn:de:0030-drops-248719},
  doi =		{10.4230/LIPIcs.DISC.2025.55},
  annote =	{Keywords: shared-memory, data structure, double-ended, priority queue, priority deque, heap, skip list, combining}
}
Document
Brief Announcement
DOI: 10.4230/LIPIcs.DISC.2025.62
Brief Announcement: Time, Fences and the Ordering of Events in TSO

Authors: Raïssa Nataf and Yoram Moses

Published in: LIPIcs, Volume 356, 39th International Symposium on Distributed Computing (DISC 2025)

Abstract
Total Store Order (TSO) is one of the most popular relaxed memory model in multiprocessor architectures, widely implemented, for example, in Intel’s x86 and x64 platforms. It delays write visibility via store buffers, thereby allowing a significant improvement in efficiency. This, however, complicates reasoning about correctness, as executions may violate sequential consistency. We present a semantic framework that provides effective tools that can pinpoint when such synchronization is necessary under TSO. We define a TSO-specific occurs-before relation, adapting Lamport’s happens-before to TSO, and prove that events at different sites can be temporally ordered only via an occurs-before chain. Analyzing how fences and RMWs create these chains lets us identify when they are unavoidable. We present in this BA how these results impact linearizable implementations of registers, capturing information flow and causality in TSO. The full version of this work provides details as well as results regarding the need for synchronization in linearizable implementations of additional objects.
Cite as

Raïssa Nataf and Yoram Moses. Brief Announcement: Time, Fences and the Ordering of Events in TSO. In 39th International Symposium on Distributed Computing (DISC 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 356, pp. 62:1-62:7, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{nataf_et_al:LIPIcs.DISC.2025.62,
  author =	{Nataf, Ra\"{i}ssa and Moses, Yoram},
  title =	{{Brief Announcement: Time, Fences and the Ordering of Events in TSO}},
  booktitle =	{39th International Symposium on Distributed Computing (DISC 2025)},
  pages =	{62:1--62:7},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-402-4},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{356},
  editor =	{Kowalski, Dariusz R.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.DISC.2025.62},
  URN =		{urn:nbn:de:0030-drops-248784},
  doi =		{10.4230/LIPIcs.DISC.2025.62},
  annote =	{Keywords: TSO, linearizability, happens before, fences, synchronization actions}
}
Document
DOI: 10.4230/LIPIcs.ESA.2025.85
A Simple yet Exact Analysis of the MultiQueue

Authors: Stefan Walzer and Marvin Williams

Published in: LIPIcs, Volume 351, 33rd Annual European Symposium on Algorithms (ESA 2025)

Abstract
The MultiQueue is a relaxed concurrent priority queue consisting of n internal priority queues, where an insertion uses a random queue and a deletion considers two random queues and deletes the minimum from the one with the smaller minimum. The rank error of the deletion is the number of smaller elements in the MultiQueue. Alistarh et al. [Alistarh et al., 2017] have demonstrated in a sophisticated potential argument that the expected rank error remains bounded by 𝒪(n) over long sequences of deletions. In this paper we present a simpler analysis by identifying the stable distribution of an underlying Markov chain and with it the long-term distribution of the rank error exactly. Simple calculations then reveal the expected long-term rank error to be (5/6)n-1+1/(6n). Our arguments generalize to deletion schemes where the probability to delete from a given queue depends only on the rank of the queue. Specifically, this includes deleting from the best of c randomly selected queues for any c > 1.
Cite as

Stefan Walzer and Marvin Williams. A Simple yet Exact Analysis of the MultiQueue. In 33rd Annual European Symposium on Algorithms (ESA 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 351, pp. 85:1-85:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{walzer_et_al:LIPIcs.ESA.2025.85,
  author =	{Walzer, Stefan and Williams, Marvin},
  title =	{{A Simple yet Exact Analysis of the MultiQueue}},
  booktitle =	{33rd Annual European Symposium on Algorithms (ESA 2025)},
  pages =	{85:1--85:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-395-9},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{351},
  editor =	{Benoit, Anne and Kaplan, Haim and Wild, Sebastian and Herman, Grzegorz},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ESA.2025.85},
  URN =		{urn:nbn:de:0030-drops-245533},
  doi =		{10.4230/LIPIcs.ESA.2025.85},
  annote =	{Keywords: MultiQueue, concurrent data structure, stochastic process, Markov chain}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2025.26
Optimal Concolic Dynamic Partial Order Reduction

Authors: Mohammad Hossein Khoshechin Jorshari, Michalis Kokologiannakis, Rupak Majumdar, and Srinidhi Nagendra

Published in: LIPIcs, Volume 348, 36th International Conference on Concurrency Theory (CONCUR 2025)

Abstract
Stateless model checking (SMC) software implementations requires exploring both concurrency- and data nondeterminism. Unfortunately, most SMC algorithms focus on efficient exploration of concurrency nondeterminism, thereby neglecting an important source of bugs. We present ConDpor, an SMC algorithm for unmodified Java programs that combines optimal dynamic partial order reduction (DPOR) for concurrency nondeterminism, with concolic execution for data nondeterminism. ConDpor is sound, complete, optimal, and parametric w.r.t. the memory consistency model. Our experiments confirm that ConDpor is exponentially faster than DPOR with small-domain enumeration. Overall, ConDpor opens the door for efficient exploration of concurrent programs with data nondeterminism.
Cite as

Mohammad Hossein Khoshechin Jorshari, Michalis Kokologiannakis, Rupak Majumdar, and Srinidhi Nagendra. Optimal Concolic Dynamic Partial Order Reduction. In 36th International Conference on Concurrency Theory (CONCUR 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 348, pp. 26:1-26:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{khoshechinjorshari_et_al:LIPIcs.CONCUR.2025.26,
  author =	{Khoshechin Jorshari, Mohammad Hossein and Kokologiannakis, Michalis and Majumdar, Rupak and Nagendra, Srinidhi},
  title =	{{Optimal Concolic Dynamic Partial Order Reduction}},
  booktitle =	{36th International Conference on Concurrency Theory (CONCUR 2025)},
  pages =	{26:1--26:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-389-8},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{348},
  editor =	{Bouyer, Patricia and van de Pol, Jaco},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2025.26},
  URN =		{urn:nbn:de:0030-drops-239765},
  doi =		{10.4230/LIPIcs.CONCUR.2025.26},
  annote =	{Keywords: Stateless model checking, dynamic symbolic execution}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2025.17
Just Verification of Mutual Exclusion Algorithms

Authors: Rob van Glabbeek, Bas Luttik, and Myrthe S. C. Spronck

Published in: LIPIcs, Volume 348, 36th International Conference on Concurrency Theory (CONCUR 2025)

Abstract
We verify the correctness of a variety of mutual exclusion algorithms through model checking. We look at algorithms where communication is via shared read/write registers, where those registers can be atomic or non-atomic. For the verification of liveness properties, it is necessary to assume a completeness criterion to eliminate spurious counterexamples. We use justness as completeness criterion. Justness depends on a concurrency relation; we consider several such relations, modelling different assumptions on the working of the shared registers. We present executions demonstrating the violation of correctness properties by several algorithms, and in some cases suggest improvements.
Cite as

Rob van Glabbeek, Bas Luttik, and Myrthe S. C. Spronck. Just Verification of Mutual Exclusion Algorithms. In 36th International Conference on Concurrency Theory (CONCUR 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 348, pp. 17:1-17:25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{vanglabbeek_et_al:LIPIcs.CONCUR.2025.17,
  author =	{van Glabbeek, Rob and Luttik, Bas and Spronck, Myrthe S. C.},
  title =	{{Just Verification of Mutual Exclusion Algorithms}},
  booktitle =	{36th International Conference on Concurrency Theory (CONCUR 2025)},
  pages =	{17:1--17:25},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-389-8},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{348},
  editor =	{Bouyer, Patricia and van de Pol, Jaco},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2025.17},
  URN =		{urn:nbn:de:0030-drops-239670},
  doi =		{10.4230/LIPIcs.CONCUR.2025.17},
  annote =	{Keywords: Mutual exclusion, safe registers, regular registers, overlapping reads and writes, atomicity, safety, liveness, starvation freedom, justness, model checking, mCRL2}
}
Document
DOI: 10.4230/LIPIcs.OPODIS.2024.6
DULL: A Fast Scalable Detectable Unrolled Lock-Based Linked List

Authors: Ahmed Fahmy and Wojciech Golab

Published in: LIPIcs, Volume 324, 28th International Conference on Principles of Distributed Systems (OPODIS 2024)

Abstract
Persistent memory (PM) has emerged as a promising technology that enables data structures to preserve their consistent state after recovering from system failures. Detectable data structures have been proposed to detect the response of the last operation of a crashed process. Various lock-free detectable and recoverable concurrent data structures have been developed in the literature. However, designing detectable lock-based structures is challenging due to the need to preserve the correctness properties of the underlying locks, such as mutual exclusion and deadlock-freedom, across failures. Therefore, lock-based detectable and persistent data structures are not as common as lock-free structures. In this work, we introduce DULL: a fast, scalable and Detectable Unrolled Lock-based Linked list. This paper presents the design and implementation of DULL, along with an evaluation of its recoverability and scalability. Experimental Results show that DULL is several-fold faster than the competition in all workloads that involve updates. Moreover, as opposed to some of the previous works, our algorithm is scalable when the multiprocessor is oversubscribed. DULL is a demonstration of the feasibility of using lock-based data structures with detectability in PM environments. We believe that DULL opens up new research directions for designing and analyzing detectable lock-based data structures.
Cite as

Ahmed Fahmy and Wojciech Golab. DULL: A Fast Scalable Detectable Unrolled Lock-Based Linked List. In 28th International Conference on Principles of Distributed Systems (OPODIS 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 324, pp. 6:1-6:25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{fahmy_et_al:LIPIcs.OPODIS.2024.6,
  author =	{Fahmy, Ahmed and Golab, Wojciech},
  title =	{{DULL: A Fast Scalable Detectable Unrolled Lock-Based Linked List}},
  booktitle =	{28th International Conference on Principles of Distributed Systems (OPODIS 2024)},
  pages =	{6:1--6:25},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-360-7},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{324},
  editor =	{Bonomi, Silvia and Galletta, Letterio and Rivi\`{e}re, Etienne and Schiavoni, Valerio},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.OPODIS.2024.6},
  URN =		{urn:nbn:de:0030-drops-225429},
  doi =		{10.4230/LIPIcs.OPODIS.2024.6},
  annote =	{Keywords: detectability, lock-based, mutual exclusion, linked list, fault-tolerance, persistent memory, concurrency}
}
Document
DOI: 10.4230/LIPIcs.OPODIS.2024.5
RMR-Efficient Detectable Objects for Persistent Memory and Their Applications

Authors: Sahil Dhoked, Ahmed Fahmy, Wojciech Golab, and Neeraj Mittal

Published in: LIPIcs, Volume 324, 28th International Conference on Principles of Distributed Systems (OPODIS 2024)

Abstract
We describe a novel construction of arbitrary read-modify-write (RMW) primitives in a persistent shared memory model with process failures. Our construction uses blocking synchronization, in the form of recoverable mutual exclusion (RME), and is optimal in terms of the widely studied remote memory reference (RMR) complexity measure. The implemented objects tolerate either system-wide or independent process crashes, depending on the RME lock used, and also provide detectability for resolving the outcome of operations interrupted by failures. We prove that our construction is RMR-optimal using a reduction back to the RME problem. Our proof technique introduces a novel algorithmic style that enables solving challenging synchronization problems using a common execution path for both the system-wide and independent failure models, which previously required separate analyses, and relies only on a suitable implementation of the detectable base objects in each model to achieve RMR efficiency. Experiments demonstrate that our construction outperforms prior wait-free and lock-free algorithms on a multiprocessor with Intel Optane persistent memory.
Cite as

Sahil Dhoked, Ahmed Fahmy, Wojciech Golab, and Neeraj Mittal. RMR-Efficient Detectable Objects for Persistent Memory and Their Applications. In 28th International Conference on Principles of Distributed Systems (OPODIS 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 324, pp. 5:1-5:26, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{dhoked_et_al:LIPIcs.OPODIS.2024.5,
  author =	{Dhoked, Sahil and Fahmy, Ahmed and Golab, Wojciech and Mittal, Neeraj},
  title =	{{RMR-Efficient Detectable Objects for Persistent Memory and Their Applications}},
  booktitle =	{28th International Conference on Principles of Distributed Systems (OPODIS 2024)},
  pages =	{5:1--5:26},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-360-7},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{324},
  editor =	{Bonomi, Silvia and Galletta, Letterio and Rivi\`{e}re, Etienne and Schiavoni, Valerio},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.OPODIS.2024.5},
  URN =		{urn:nbn:de:0030-drops-225417},
  doi =		{10.4230/LIPIcs.OPODIS.2024.5},
  annote =	{Keywords: persistent memory, synchronization, recoverability, fault tolerance, detectability, scalability, RMR complexity, theory, mutual exclusion}
}
Document
Position
DOI: 10.4230/TGDK.2.1.5
Standardizing Knowledge Engineering Practices with a Reference Architecture

Authors: Bradley P. Allen and Filip Ilievski

Published in: TGDK, Volume 2, Issue 1 (2024): Special Issue on Trends in Graph Data and Knowledge - Part 2. Transactions on Graph Data and Knowledge, Volume 2, Issue 1

Abstract
Knowledge engineering is the process of creating and maintaining knowledge-producing systems. Throughout the history of computer science and AI, knowledge engineering workflows have been widely used given the importance of high-quality knowledge for reliable intelligent agents. Meanwhile, the scope of knowledge engineering, as apparent from its target tasks and use cases, has been shifting, together with its paradigms such as expert systems, semantic web, and language modeling. The intended use cases and supported user requirements between these paradigms have not been analyzed globally, as new paradigms often satisfy prior pain points while possibly introducing new ones. The recent abstraction of systemic patterns into a boxology provides an opening for aligning the requirements and use cases of knowledge engineering with the systems, components, and software that can satisfy them best, however, this direction has not been explored to date. This paper proposes a vision of harmonizing the best practices in the field of knowledge engineering by leveraging the software engineering methodology of creating reference architectures. We describe how a reference architecture can be iteratively designed and implemented to associate user needs with recurring systemic patterns, building on top of existing knowledge engineering workflows and boxologies. We provide a six-step roadmap that can enable the development of such an architecture, consisting of scope definition, selection of information sources, architectural analysis, synthesis of an architecture based on the information source analysis, evaluation through instantiation, and, ultimately, instantiation into a concrete software architecture. We provide an initial design and outcome of the definition of architectural scope, selection of information sources, and analysis. As the remaining steps of design, evaluation, and instantiation of the architecture are largely use-case specific, we provide a detailed description of their procedures and point to relevant examples. We expect that following through on this vision will lead to well-grounded reference architectures for knowledge engineering, will advance the ongoing initiatives of organizing the neurosymbolic knowledge engineering space, and will build new links to the software architectures and data science communities.
Cite as

Bradley P. Allen and Filip Ilievski. Standardizing Knowledge Engineering Practices with a Reference Architecture. In Special Issue on Trends in Graph Data and Knowledge - Part 2. Transactions on Graph Data and Knowledge (TGDK), Volume 2, Issue 1, pp. 5:1-5:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@Article{allen_et_al:TGDK.2.1.5,
  author =	{Allen, Bradley P. and Ilievski, Filip},
  title =	{{Standardizing Knowledge Engineering Practices with a Reference Architecture}},
  journal =	{Transactions on Graph Data and Knowledge},
  pages =	{5:1--5:23},
  ISSN =	{2942-7517},
  year =	{2024},
  volume =	{2},
  number =	{1},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/TGDK.2.1.5},
  URN =		{urn:nbn:de:0030-drops-198623},
  doi =		{10.4230/TGDK.2.1.5},
  annote =	{Keywords: knowledge engineering, knowledge graphs, quality attributes, software architectures, sociotechnical systems}
}
Document
DOI: 10.4230/LIPIcs.OPODIS.2023.24
Recoverable and Detectable Self-Implementations of Swap

Authors: Tomer Lev Lehman, Hagit Attiya, and Danny Hendler

Published in: LIPIcs, Volume 286, 27th International Conference on Principles of Distributed Systems (OPODIS 2023)

Abstract
Recoverable algorithms tolerate failures and recoveries of processes by using non-volatile memory. Of particular interest are self-implementations of key operations, in which a recoverable operation is implemented from its non-recoverable counterpart (in addition to reads and writes). This paper presents two self-implementations of the swap operation. One works in the system-wide failures model, where all processes fail and recover together, and the other in the independent failures model, where each process crashes and recovers independently of the other processes. Both algorithms are wait-free in crash-free executions, but their recovery code is blocking. We prove that this is inherent for the independent failures model. The impossibility result is proved for implementations of distinguishable operations using interfering functions, and in particular, it applies to a recoverable self-implementation of swap.
Cite as

Tomer Lev Lehman, Hagit Attiya, and Danny Hendler. Recoverable and Detectable Self-Implementations of Swap. In 27th International Conference on Principles of Distributed Systems (OPODIS 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 286, pp. 24:1-24:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{levlehman_et_al:LIPIcs.OPODIS.2023.24,
  author =	{Lev Lehman, Tomer and Attiya, Hagit and Hendler, Danny},
  title =	{{Recoverable and Detectable Self-Implementations of Swap}},
  booktitle =	{27th International Conference on Principles of Distributed Systems (OPODIS 2023)},
  pages =	{24:1--24:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-308-9},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{286},
  editor =	{Bessani, Alysson and D\'{e}fago, Xavier and Nakamura, Junya and Wada, Koichi and Yamauchi, Yukiko},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.OPODIS.2023.24},
  URN =		{urn:nbn:de:0030-drops-195140},
  doi =		{10.4230/LIPIcs.OPODIS.2023.24},
  annote =	{Keywords: Multi-core algorithms, persistent memory, non-volatile memory, recoverable objects, detectablitly}
}
  • Refine by Type
  • 19 Document/PDF
  • 14 Document/HTML

  • Refine by Publication Year
  • 2 2026
  • 11 2025
  • 2 2024
  • 1 2023
  • 1 2022
  • Show More...

  • Refine by Author
  • 5 Attiya, Hagit
  • 5 Hendler, Danny
  • 3 Fatourou, Panagiota
  • 2 Ellen, Faith
  • 2 Fahmy, Ahmed
  • Show More...

  • Refine by Series/Journal
  • 17 LIPIcs
  • 2 TGDK

  • Refine by Classification
  • 6 Theory of computation → Concurrent algorithms
  • 6 Theory of computation → Shared memory algorithms
  • 4 Theory of computation → Data structures design and analysis
  • 3 Theory of computation → Concurrency
  • 2 Theory of computation → Distributed algorithms
  • Show More...

  • Refine by Keyword
  • 4 persistent memory
  • 3 non-volatile memory
  • 2 Concurrent Data Structures
  • 2 Multi-core algorithms
  • 2 Shared Memory
  • Show More...

Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact