5 Search Results for "Luchangco, Victor"


Document
Invited Talk
Theory Meets Practice in the Algorand Blockchain (Invited Talk)

Authors: Victor Luchangco

Published in: LIPIcs, Volume 253, 26th International Conference on Principles of Distributed Systems (OPODIS 2022)


Abstract
Robust and effective distributed systems require good theory and good engineering, not separately but in concert: user requirements and system constraints are not merely implementation details but often must inform the design of algorithms for such systems. Blockchains are an excellent example. The heart of a blockchain is its (Byzantine) consensus protocol, and consensus protocols have been extensively studied in the theory community for decades. But traditional consensus protocols are not directly applicable to blockchains, which have, or hope to have, millions of participants. Furthermore, public blockchains, which allow anyone to participate, must have some mechanism to guarantee the security of the protocol, and traditional fault models do not adequately capture the assumptions of such mechanisms. In this talk, I will discuss these and other ways in which theory and practice meet in the context of the Algorand blockchain, and how Algorand is able to achieve high transaction throughput with low latency.

Cite as

Victor Luchangco. Theory Meets Practice in the Algorand Blockchain (Invited Talk). In 26th International Conference on Principles of Distributed Systems (OPODIS 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 253, p. 1:1, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2023)


Copy BibTex To Clipboard

@InProceedings{luchangco:LIPIcs.OPODIS.2022.1,
  author =	{Luchangco, Victor},
  title =	{{Theory Meets Practice in the Algorand Blockchain}},
  booktitle =	{26th International Conference on Principles of Distributed Systems (OPODIS 2022)},
  pages =	{1:1--1:1},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-265-5},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{253},
  editor =	{Hillel, Eshcar and Palmieri, Roberto and Rivi\`{e}re, Etienne},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.OPODIS.2022.1},
  URN =		{urn:nbn:de:0030-drops-176219},
  doi =		{10.4230/LIPIcs.OPODIS.2022.1},
  annote =	{Keywords: Theory and practice, Design of distributed systems, Blockchain, Consensus, Algorand}
}
Document
Polynomial-Time Verification and Testing of Implementations of the Snapshot Data Structure

Authors: Gal Amram, Avi Hayoun, Lior Mizrahi, and Gera Weiss

Published in: LIPIcs, Volume 246, 36th International Symposium on Distributed Computing (DISC 2022)


Abstract
We analyze correctness of implementations of the snapshot data structure in terms of linearizability. We show that such implementations can be verified in polynomial time. Additionally, we identify a set of representative executions for testing and show that the correctness of each of these executions can be validated in linear time. These results present a significant speedup considering that verifying linearizability of implementations of concurrent data structures, in general, is EXPSPACE-complete in the number of program-states, and testing linearizability is NP-complete in the length of the tested execution. The crux of our approach is identifying a class of executions, which we call simple, such that a snapshot implementation is linearizable if and only if all of its simple executions are linearizable. We then divide all possible non-linearizable simple executions into three categories and construct a small automaton that recognizes each category. We describe two implementations (one for verification and one for testing) of an automata-based approach that we develop based on this result and an evaluation that demonstrates significant improvements over existing tools. For verification, we show that restricting a state-of-the-art tool to analyzing only simple executions saves resources and allows the analysis of more complex cases. Specifically, restricting attention to simple executions finds bugs in 27 instances, whereas, without this restriction, we were only able to find 14 of the 30 bugs in the instances we examined. We also show that our technique accelerates testing performance significantly. Specifically, our implementation solves the complete set of 900 problems we generated, whereas the state-of-the-art linearizability testing tool solves only 554 problems.

Cite as

Gal Amram, Avi Hayoun, Lior Mizrahi, and Gera Weiss. Polynomial-Time Verification and Testing of Implementations of the Snapshot Data Structure. In 36th International Symposium on Distributed Computing (DISC 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 246, pp. 5:1-5:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)


Copy BibTex To Clipboard

@InProceedings{amram_et_al:LIPIcs.DISC.2022.5,
  author =	{Amram, Gal and Hayoun, Avi and Mizrahi, Lior and Weiss, Gera},
  title =	{{Polynomial-Time Verification and Testing of Implementations of the Snapshot Data Structure}},
  booktitle =	{36th International Symposium on Distributed Computing (DISC 2022)},
  pages =	{5:1--5:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-255-6},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{246},
  editor =	{Scheideler, Christian},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.DISC.2022.5},
  URN =		{urn:nbn:de:0030-drops-171964},
  doi =		{10.4230/LIPIcs.DISC.2022.5},
  annote =	{Keywords: Snapshot, Linearizability, Verification, Formal Methods}
}
Document
Deep Static Modeling of invokedynamic

Authors: George Fourtounis and Yannis Smaragdakis

Published in: LIPIcs, Volume 134, 33rd European Conference on Object-Oriented Programming (ECOOP 2019)


Abstract
Java 7 introduced programmable dynamic linking in the form of the invokedynamic framework. Static analysis of code containing programmable dynamic linking has often been cited as a significant source of unsoundness in the analysis of Java programs. For example, Java lambdas, introduced in Java 8, are a very popular feature, which is, however, resistant to static analysis, since it mixes invokedynamic with dynamic code generation. These techniques invalidate static analysis assumptions: programmable linking breaks reasoning about method resolution while dynamically generated code is, by definition, not available statically. In this paper, we show that a static analysis can predictively model uses of invokedynamic while also cooperating with extra rules to handle the runtime code generation of lambdas. Our approach plugs into an existing static analysis and helps eliminate all unsoundness in the handling of lambdas (including associated features such as method references) and generic invokedynamic uses. We evaluate our technique on a benchmark suite of our own and on third-party benchmarks, uncovering all code previously unreachable due to unsoundness, highly efficiently.

Cite as

George Fourtounis and Yannis Smaragdakis. Deep Static Modeling of invokedynamic. In 33rd European Conference on Object-Oriented Programming (ECOOP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 134, pp. 15:1-15:28, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)


Copy BibTex To Clipboard

@InProceedings{fourtounis_et_al:LIPIcs.ECOOP.2019.15,
  author =	{Fourtounis, George and Smaragdakis, Yannis},
  title =	{{Deep Static Modeling of invokedynamic}},
  booktitle =	{33rd European Conference on Object-Oriented Programming (ECOOP 2019)},
  pages =	{15:1--15:28},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-111-5},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{134},
  editor =	{Donaldson, Alastair F.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2019.15},
  URN =		{urn:nbn:de:0030-drops-108076},
  doi =		{10.4230/LIPIcs.ECOOP.2019.15},
  annote =	{Keywords: static analysis, invokedynamic}
}
Document
DynaSOAr: A Parallel Memory Allocator for Object-Oriented Programming on GPUs with Efficient Memory Access

Authors: Matthias Springer and Hidehiko Masuhara

Published in: LIPIcs, Volume 134, 33rd European Conference on Object-Oriented Programming (ECOOP 2019)


Abstract
Object-oriented programming has long been regarded as too inefficient for SIMD high-performance computing, despite the fact that many important HPC applications have an inherent object structure. On SIMD accelerators, including GPUs, this is mainly due to performance problems with memory allocation and memory access: There are a few libraries that support parallel memory allocation directly on accelerator devices, but all of them suffer from uncoalesed memory accesses. We discovered a broad class of object-oriented programs with many important real-world applications that can be implemented efficiently on massively parallel SIMD accelerators. We call this class Single-Method Multiple-Objects (SMMO), because parallelism is expressed by running a method on all objects of a type. To make fast GPU programming available to domain experts who are less experienced in GPU programming, we developed DynaSOAr, a CUDA framework for SMMO applications. DynaSOAr consists of (1) a fully-parallel, lock-free, dynamic memory allocator, (2) a data layout DSL and (3) an efficient, parallel do-all operation. DynaSOAr achieves performance superior to state-of-the-art GPU memory allocators by controlling both memory allocation and memory access. DynaSOAr improves the usage of allocated memory with a Structure of Arrays (SOA) data layout and achieves low memory fragmentation through efficient management of free and allocated memory blocks with lock-free, hierarchical bitmaps. Contrary to other allocators, our design is heavily based on atomic operations, trading raw (de)allocation performance for better overall application performance. In our benchmarks, DynaSOAr achieves a speedup of application code of up to 3x over state-of-the-art allocators. Moreover, DynaSOAr manages heap memory more efficiently than other allocators, allowing programmers to run up to 2x larger problem sizes with the same amount of memory.

Cite as

Matthias Springer and Hidehiko Masuhara. DynaSOAr: A Parallel Memory Allocator for Object-Oriented Programming on GPUs with Efficient Memory Access. In 33rd European Conference on Object-Oriented Programming (ECOOP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 134, pp. 17:1-17:37, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)


Copy BibTex To Clipboard

@InProceedings{springer_et_al:LIPIcs.ECOOP.2019.17,
  author =	{Springer, Matthias and Masuhara, Hidehiko},
  title =	{{DynaSOAr: A Parallel Memory Allocator for Object-Oriented Programming on GPUs with Efficient Memory Access}},
  booktitle =	{33rd European Conference on Object-Oriented Programming (ECOOP 2019)},
  pages =	{17:1--17:37},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-111-5},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{134},
  editor =	{Donaldson, Alastair F.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2019.17},
  URN =		{urn:nbn:de:0030-drops-108098},
  doi =		{10.4230/LIPIcs.ECOOP.2019.17},
  annote =	{Keywords: CUDA, Data Layout, Dynamic Memory Allocation, GPUs, Object-oriented Programming, SIMD, Single-Instruction Multiple-Objects, Structure of Arrays}
}
Document
Extending Transactional Memory with Atomic Deferral

Authors: Tingzhe Zhou, Victor Luchangco, and Michael Spear

Published in: LIPIcs, Volume 95, 21st International Conference on Principles of Distributed Systems (OPODIS 2017)


Abstract
This paper introduces atomic deferral, an extension to TM that allows programmers to move long-running or irrevocable operations out of a transaction while maintaining serializability: the transaction and its de- ferred operation appear to execute atomically from the perspective of other transactions. Thus, program- mers can adapt lock-based programs to exploit TM with relatively little effort and without sacrificing scalability by atomically deferring the problematic operations. We demonstrate this with several use cases for atomic deferral, as well as an in-depth analysis of its use on the PARSEC dedup benchmark, where we show that atomic deferral enables TM to be competitive with well-designed lock-based code.

Cite as

Tingzhe Zhou, Victor Luchangco, and Michael Spear. Extending Transactional Memory with Atomic Deferral. In 21st International Conference on Principles of Distributed Systems (OPODIS 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 95, pp. 7:1-7:17, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2018)


Copy BibTex To Clipboard

@InProceedings{zhou_et_al:LIPIcs.OPODIS.2017.7,
  author =	{Zhou, Tingzhe and Luchangco, Victor and Spear, Michael},
  title =	{{Extending Transactional Memory with Atomic Deferral}},
  booktitle =	{21st International Conference on Principles of Distributed Systems (OPODIS 2017)},
  pages =	{7:1--7:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-061-3},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{95},
  editor =	{Aspnes, James and Bessani, Alysson and Felber, Pascal and Leit\~{a}o, Jo\~{a}o},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.OPODIS.2017.7},
  URN =		{urn:nbn:de:0030-drops-86275},
  doi =		{10.4230/LIPIcs.OPODIS.2017.7},
  annote =	{Keywords: Transactional Memory, Concurrency, Synchronization, I/O}
}
  • Refine by Author
  • 2 Luchangco, Victor
  • 1 Amram, Gal
  • 1 Fourtounis, George
  • 1 Hayoun, Avi
  • 1 Masuhara, Hidehiko
  • Show More...

  • Refine by Classification
  • 1 Computer systems organization → Dependable and fault-tolerant systems and networks
  • 1 Computer systems organization → Single instruction, multiple data
  • 1 Software and its engineering → Allocation / deallocation strategies
  • 1 Software and its engineering → Compilers
  • 1 Software and its engineering → Formal software verification
  • Show More...

  • Refine by Keyword
  • 1 Algorand
  • 1 Blockchain
  • 1 CUDA
  • 1 Concurrency
  • 1 Consensus
  • Show More...

  • Refine by Type
  • 5 document

  • Refine by Publication Year
  • 2 2019
  • 1 2018
  • 1 2022
  • 1 2023

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