6 Search Results for "Bender, John"

Document
DOI: 10.4230/LIPIcs.ISAAC.2022.21
External-Memory Dictionaries with Worst-Case Update Cost

Authors: Rathish Das, John Iacono, and Yakov Nekrich

Published in: LIPIcs, Volume 248, 33rd International Symposium on Algorithms and Computation (ISAAC 2022)

Abstract
The B^ε-tree [Brodal and Fagerberg 2003] is a simple I/O-efficient external-memory-model data structure that supports updates orders of magnitude faster than B-tree with a query performance comparable to the B-tree: for any positive constant ε < 1 insertions and deletions take O(1/B^(1-ε) log_B N) time (rather than O(log_BN) time for the classic B-tree), queries take O(log_B N) time and range queries returning k items take O(log_B N + k/B) time. Although the B^ε-tree has an optimal update/query tradeoff, the runtimes are amortized. Another structure, the write-optimized skip list, introduced by Bender et al. [PODS 2017], has the same performance as the B^ε-tree but with runtimes that are randomized rather than amortized. In this paper, we present a variant of the B^ε-tree with deterministic worst-case running times that are identical to the original’s amortized running times.
Cite as

Rathish Das, John Iacono, and Yakov Nekrich. External-Memory Dictionaries with Worst-Case Update Cost. In 33rd International Symposium on Algorithms and Computation (ISAAC 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 248, pp. 21:1-21:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{das_et_al:LIPIcs.ISAAC.2022.21,
  author =	{Das, Rathish and Iacono, John and Nekrich, Yakov},
  title =	{{External-Memory Dictionaries with Worst-Case Update Cost}},
  booktitle =	{33rd International Symposium on Algorithms and Computation (ISAAC 2022)},
  pages =	{21:1--21:13},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-258-7},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{248},
  editor =	{Bae, Sang Won and Park, Heejin},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ISAAC.2022.21},
  URN =		{urn:nbn:de:0030-drops-173060},
  doi =		{10.4230/LIPIcs.ISAAC.2022.21},
  annote =	{Keywords: Data Structures, External Memory, Buffer Tree}
}
Document
Artifact
DOI: 10.4230/DARTS.8.2.3
Compiling Volatile Correctly in Java (Artifact)

Authors: Shuyang Liu, John Bender, and Jens Palsberg

Published in: DARTS, Volume 8, Issue 2, Special Issue of the 36th European Conference on Object-Oriented Programming (ECOOP 2022)

Abstract
The compilation scheme for Volatile accesses in the OpenJDK 9 HotSpot Java Virtual Machine has a major problem that persists despite a recent bug report and a long discussion. One of the suggested fixes is to let Java compile Volatile accesses in the same way as C/C++11. However, we show that this approach is invalid for Java. Indeed, we show a set of optimizations that is valid for C/C++11 but invalid for Java, while the compilation scheme is similar. We prove the correctness of the compilation scheme to Power and x86 and a suite of valid optimizations in Java. Our proofs are based on a language model that we validate by proving key properties such as the DRF-SC theorem and by running litmus tests via our implementation of Java in Herd7.
Cite as

Shuyang Liu, John Bender, and Jens Palsberg. Compiling Volatile Correctly in Java (Artifact). In Special Issue of the 36th European Conference on Object-Oriented Programming (ECOOP 2022). Dagstuhl Artifacts Series (DARTS), Volume 8, Issue 2, pp. 3:1-3:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@Article{liu_et_al:DARTS.8.2.3,
  author =	{Liu, Shuyang and Bender, John and Palsberg, Jens},
  title =	{{Compiling Volatile Correctly in Java (Artifact)}},
  pages =	{3:1--3:2},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2022},
  volume =	{8},
  number =	{2},
  editor =	{Liu, Shuyang and Bender, John and Palsberg, Jens},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DARTS.8.2.3},
  URN =		{urn:nbn:de:0030-drops-162018},
  doi =		{10.4230/DARTS.8.2.3},
  annote =	{Keywords: formal semantics, concurrency, compilation}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2022.6
Compiling Volatile Correctly in Java

Authors: Shuyang Liu, John Bender, and Jens Palsberg

Published in: LIPIcs, Volume 222, 36th European Conference on Object-Oriented Programming (ECOOP 2022)

Abstract
The compilation scheme for Volatile accesses in the OpenJDK 9 HotSpot Java Virtual Machine has a major problem that persists despite a recent bug report and a long discussion. One of the suggested fixes is to let Java compile Volatile accesses in the same way as C/C++11. However, we show that this approach is invalid for Java. Indeed, we show a set of optimizations that is valid for C/C++11 but invalid for Java, while the compilation scheme is similar. We prove the correctness of the compilation scheme to Power and x86 and a suite of valid optimizations in Java. Our proofs are based on a language model that we validate by proving key properties such as the DRF-SC theorem and by running litmus tests via our implementation of Java in Herd7.
Cite as

Shuyang Liu, John Bender, and Jens Palsberg. Compiling Volatile Correctly in Java. In 36th European Conference on Object-Oriented Programming (ECOOP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 222, pp. 6:1-6:26, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{liu_et_al:LIPIcs.ECOOP.2022.6,
  author =	{Liu, Shuyang and Bender, John and Palsberg, Jens},
  title =	{{Compiling Volatile Correctly in Java}},
  booktitle =	{36th European Conference on Object-Oriented Programming (ECOOP 2022)},
  pages =	{6:1--6:26},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-225-9},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{222},
  editor =	{Ali, Karim and Vitek, Jan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2022.6},
  URN =		{urn:nbn:de:0030-drops-162346},
  doi =		{10.4230/LIPIcs.ECOOP.2022.6},
  annote =	{Keywords: formal semantics, concurrency, compilation}
}
Document
DOI: 10.4230/LIPIcs.FUN.2021.19
Train Tracks with Gaps

Authors: William Kuszmaul

Published in: LIPIcs, Volume 157, 10th International Conference on Fun with Algorithms (FUN 2021) (2020)

Abstract
We identify a tradeoff curve between the number of wheels on a train car, and the amount of track that must be installed in order to ensure that the train car is supported by the track at all times. The goal is to build an elevated track that covers some large distance 𝓁, but that consists primarily of gaps, so that the total amount of feet of train track that is actually installed is only a small fraction of 𝓁. In order so that the train track can support the train at all points, the requirement is that as the train drives across the track, at least one set of wheels from the rear quarter and at least one set of wheels from the front quarter of the train must be touching the track at all times. We show that, if a train car has n sets of wheels evenly spaced apart in its rear and n sets of wheels evenly spaced apart in its front, then it is possible to build a train track that supports the train car but uses only Θ(𝓁 / n) feet of track. We then consider what happens if the wheels on the train car are not evenly spaced (and may even be configured adversarially). We show that for any configuration of the train car, with n wheels in each of the front and rear quarters of the car, it is possible to build a track that supports the car for distance 𝓁 and uses only O((𝓁 log n)/n) feet of track. Additionally, we show that there exist configurations of the train car for which this tradeoff curve is asymptotically optimal. Both the upper and lower bounds are achieved via applications of the probabilistic method. The algorithms and lower bounds in this paper provide simple illustrative examples of many of the core techniques in probabilistic combinatorics and randomized algorithms. These include the probabilistic method with alterations, the use of McDiarmid’s inequality within the probabilistic method, the algorithmic Lovász Local Lemma, the min-hash technique, and the method of conditional probabilities.
Cite as

William Kuszmaul. Train Tracks with Gaps. In 10th International Conference on Fun with Algorithms (FUN 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 157, pp. 19:1-19:11, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{kuszmaul:LIPIcs.FUN.2021.19,
  author =	{Kuszmaul, William},
  title =	{{Train Tracks with Gaps}},
  booktitle =	{10th International Conference on Fun with Algorithms (FUN 2021)},
  pages =	{19:1--19:11},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-145-0},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{157},
  editor =	{Farach-Colton, Martin and Prencipe, Giuseppe and Uehara, Ryuhei},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FUN.2021.19},
  URN =		{urn:nbn:de:0030-drops-127800},
  doi =		{10.4230/LIPIcs.FUN.2021.19},
  annote =	{Keywords: probabilistic method, algorithms, trains, Lov\'{a}sz Local Lemma, McDiarmid’s Inequality}
}
Document
DOI: 10.4230/LIPIcs.ESA.2019.60
External Memory Priority Queues with Decrease-Key and Applications to Graph Algorithms

Authors: John Iacono, Riko Jacob, and Konstantinos Tsakalidis

Published in: LIPIcs, Volume 144, 27th Annual European Symposium on Algorithms (ESA 2019)

Abstract
We present priority queues in the external memory model with block size B and main memory size M that support on N elements, operation Update (a combination of operations Insert and DecreaseKey) in O(1/Blog_{M/B} N/B) amortized I/Os and operations ExtractMin and Delete in O(ceil[(M^epsilon)/B log_{M/B} N/B] log_{M/B} N/B) amortized I/Os, for any real epsilon in (0,1), using O(N/Blog_{M/B} N/B) blocks. Previous I/O-efficient priority queues either support these operations in O(1/Blog_2 N/B) amortized I/Os [Kumar and Schwabe, SPDP '96] or support only operations Insert, Delete and ExtractMin in optimal O(1/Blog_{M/B} N/B) amortized I/Os, however without supporting DecreaseKey [Fadel et al., TCS '99]. We also present buffered repository trees that support on a multi-set of N elements, operation Insert in O(1/Blog_M/B N/B) I/Os and operation Extract on K extracted elements in O(M^{epsilon} log_M/B N/B + K/B) amortized I/Os, using O(N/B) blocks. Previous results achieve O(1/Blog_2 N/B) I/Os and O(log_2 N/B + K/B) I/Os, respectively [Buchsbaum et al., SODA '00]. Our results imply improved O(E/Blog_{M/B} E/B) I/Os for single-source shortest paths, depth-first search and breadth-first search algorithms on massive directed dense graphs (V,E) with E = Omega (V^(1+epsilon)), epsilon > 0 and V = Omega (M), which is equal to the I/O-optimal bound for sorting E values in external memory.
Cite as

John Iacono, Riko Jacob, and Konstantinos Tsakalidis. External Memory Priority Queues with Decrease-Key and Applications to Graph Algorithms. In 27th Annual European Symposium on Algorithms (ESA 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 144, pp. 60:1-60:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{iacono_et_al:LIPIcs.ESA.2019.60,
  author =	{Iacono, John and Jacob, Riko and Tsakalidis, Konstantinos},
  title =	{{External Memory Priority Queues with Decrease-Key and Applications to Graph Algorithms}},
  booktitle =	{27th Annual European Symposium on Algorithms (ESA 2019)},
  pages =	{60:1--60:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-124-5},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{144},
  editor =	{Bender, Michael A. and Svensson, Ola and Herman, Grzegorz},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ESA.2019.60},
  URN =		{urn:nbn:de:0030-drops-111817},
  doi =		{10.4230/LIPIcs.ESA.2019.60},
  annote =	{Keywords: priority queues, external memory, graph algorithms, shortest paths, depth-first search, breadth-first search}
}
Document
DOI: 10.4230/LIPIcs.ITP.2019.18
Formal Proof and Analysis of an Incremental Cycle Detection Algorithm

Authors: Armaël Guéneau, Jacques-Henri Jourdan, Arthur Charguéraud, and François Pottier

Published in: LIPIcs, Volume 141, 10th International Conference on Interactive Theorem Proving (ITP 2019)

Abstract
We study a state-of-the-art incremental cycle detection algorithm due to Bender, Fineman, Gilbert, and Tarjan. We propose a simple change that allows the algorithm to be regarded as genuinely online. Then, we exploit Separation Logic with Time Credits to simultaneously verify the correctness and the worst-case amortized asymptotic complexity of the modified algorithm.
Cite as

Armaël Guéneau, Jacques-Henri Jourdan, Arthur Charguéraud, and François Pottier. Formal Proof and Analysis of an Incremental Cycle Detection Algorithm. In 10th International Conference on Interactive Theorem Proving (ITP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 141, pp. 18:1-18:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{gueneau_et_al:LIPIcs.ITP.2019.18,
  author =	{Gu\'{e}neau, Arma\"{e}l and Jourdan, Jacques-Henri and Chargu\'{e}raud, Arthur and Pottier, Fran\c{c}ois},
  title =	{{Formal Proof and Analysis of an Incremental Cycle Detection Algorithm}},
  booktitle =	{10th International Conference on Interactive Theorem Proving (ITP 2019)},
  pages =	{18:1--18:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-122-1},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{141},
  editor =	{Harrison, John and O'Leary, John and Tolmach, Andrew},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2019.18},
  URN =		{urn:nbn:de:0030-drops-110739},
  doi =		{10.4230/LIPIcs.ITP.2019.18},
  annote =	{Keywords: interactive deductive program verification, complexity analysis}
}
  • Refine by Author
  • 2 Bender, John
  • 2 Iacono, John
  • 2 Liu, Shuyang
  • 2 Palsberg, Jens
  • 1 Charguéraud, Arthur
  • Show More...

  • Refine by Classification
  • 2 Software and its engineering → Semantics
  • 2 Theory of computation → Data structures design and analysis
  • 2 Theory of computation → Graph algorithms analysis
  • 1 Hardware → External storage
  • 1 Software and its engineering → Correctness
  • Show More...

  • Refine by Keyword
  • 2 compilation
  • 2 concurrency
  • 2 formal semantics
  • 1 Buffer Tree
  • 1 Data Structures
  • Show More...

  • Refine by Type
  • 6 document

  • Refine by Publication Year
  • 3 2022
  • 2 2019
  • 1 2020

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

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