Publications related to Completeness and Nondeterminism in Model Checking Transactional Memories

Related publications (31)

Highly Parallel RTL Simulation

Verification and testing of hardware heavily relies on cycle-accurate simulation of RTL. As single-processor performance is growing only slowly, conventional, single-threaded RTL simulation is becoming impractical for increasingly complex chip designs and ...

EPFL2024

When is it safe to run a transactional workload under Read Committed?

Christoph Koch, Bas Ketsman

The popular isolation level multiversion Read Committed (RC) exchanges some of the strong guarantees of serializability for increased transaction throughput. Nevertheless, transaction workloads can sometimes be executed under RC while still guaranteeing se ...

ASSOC COMPUTING MACHINERY2023

One-shot Garbage Collection for In-memory OLTP through Temporality-aware Version Storage

Anastasia Ailamaki, Periklis Chrysogelos, Angelos Christos Anadiotis, Syed Mohammad Aunn Raza

Most modern in-memory online transaction processing (OLTP) engines rely on multi-version concurrency control (MVCC) to provide data consistency guarantees in the presence of conflicting data accesses. MVCC improves concurrency by generating a new version o ...

ACM2023

Compilation and Design Space Exploration of Dataflow Programs for Heterogeneous CPU-GPU Platforms

Aurélien François Gilbert Bloch

Today's continued increase in demand for processing power, despite the slowdown of Moore's law, has led to an increase in processor count, which has resulted in energy consumption and distribution problems. To address this, there is a growing trend toward ...

EPFL2023

Acceleration of Control Intensive Applications on Coarse-Grained Reconfigurable Arrays for Embedded Systems

David Atienza Alonso, Miguel Peon Quiros, Benoît Walter Denkinger

Embedded systems confront two opposite goals: low-power operation and high performance. The current trend to reach these goals is toward heterogeneous platforms, including multi-core architectures with heterogeneous cores and hardware accelerators. The lat ...

2023

Concurrency control for database theorists

Christoph Koch, Bas Ketsman

The aim of this paper is to serve as a lightweight introduction to concurrency control for database theorists through a uniform presentation of the work on robustness against Multiversion Read Committed and Snapshot Isolation. ...

ASSOC COMPUTING MACHINERY2022

A PCP Theorem for Interactive Proofs and Applications

Alessandro Chiesa

The celebrated PCP Theorem states that any language in NP can be decided via a verifier that reads O(1) bits from a polynomially long proof. Interactive oracle proofs (IOP), a generalization of PCPs, allow the verifier to interact with the prover for multi ...

SPRINGER INTERNATIONAL PUBLISHING AG2022

Micro-architectural Analysis of Database Workloads

Utku Sirin

Database workloads have significantly evolved in the past twenty years. Traditional database systems that are mainly used to serve Online Transactional Processing (OLTP) workloads evolved into specialized database systems that are optimized for particular ...

EPFL2021

Robustness against Read Committed for Transaction Templates

Christoph Koch, Bas Ketsman

The isolation level Multiversion Read Committed (RC), offered by many database systems, is known to trade consistency for increased transaction throughput. Sometimes, transaction workloads can be safely executed under RC obtaining the perfect isolation of ...

ASSOC COMPUTING MACHINERY2021

Efficient Protocols for Enforcing Causal Consistency in Geo-Replicated Key-Value Data Stores

Kristina Spirovska

Modern large-scale data platforms manage colossal amount of data, generated by the ever-increasing number of concurrent users. Geo-replicated and sharded key-value data stores play a central role when building such platforms. As the strongest consistency m ...

EPFL2020

Task scheduling for highly concurrent analytical and transaction workloads

Anastasia Ailamaki, Iraklis Psaroudakis

Systems and method for a task scheduler with dynamic adjustment of concurrency levels and task granularity are disclosed for improved execution of highly concurrent analytical and transactional systems. The task scheduler can avoid both over commitment and ...

2020

Distributed Computing with Modern Shared Memory

Mihail Igor Zablotchi

In this thesis, we revisit classic problems in shared-memory distributed computing through the lenses of (1) emerging hardware technologies and (2) changing requirements. Our contributions consist, on the one hand, in providing a better understanding of th ...

EPFL2020

Efficient Multi-Word Compare and Swap

Rachid Guerraoui, Mihail Igor Zablotchi

Atomic lock-free multi-word compare-and-swap (MCAS) is a powerful tool for designing concurrent algorithms. Yet, its widespread usage has been limited because lock-free implementations of MCAS make heavy use of expensive compare-and-swap (CAS) instructions ...

Schloss Dagstuhl, Leibniz-Zentrum2020

Distributed Transactional Systems Cannot Be Fast

Rachid Guerraoui, Willy Zwaenepoel, Diego Didona, Jingjing Wang, Panagiota Fatourou

We prove that no fully transactional system can provide fast read transactions (including read-only ones that are considered the most frequent in practice). Specifically, to achieve fast read transactions, the system has to give up support of transactions ...

2019

Fast General Distributed Transactions with Opacity

Aleksandar Dragojevic, Stanko Novakovic, Georgios Chatzopoulos

Transactions can simplify distributed applications by hiding data distribution, concurrency, and failures from the application developer. Ideally the developer would see the abstraction of a single large machine that runs transactions sequentially and neve ...

ASSOC COMPUTING MACHINERY2019

PaRiS: Causally Consistent Transactions with Non-blocking Reads and Partial Replication

Willy Zwaenepoel, Diego Didona, Kristina Spirovska

Geo-replicated data platforms are at the backbone of several large-scale online services. Transactional Causal Consistency (TCC) is an attractive consistency level for building such platforms. TCC avoids many anomalies of eventual consistency, eschews the ...

2019

PaRiS: Causally Consistent Transactions with Non-blocking Reads and Partial Replication

Willy Zwaenepoel, Diego Didona, Kristina Spirovska

Geo-replicated data platforms are the backbone of several large-scale online services. Transactional Causal Consistency (TCC) is an attractive consistency level for building such platforms. TCC avoids many anomalies of eventual consistency, eschews the syn ...

IEEE COMPUTER SOC2019

Improving Main-memory Database System Performance through Cooperative Multitasking

Georgios Psaropoulos

Database systems access memory either sequentially or randomly. Contrary to sequential access and despite the extensive efforts of computer architects, compiler writers, and system builders, random access to data larger than the processor cache has been s ...

EPFL2019

The PCL Theorem: Transactions cannot be Parallel, Consistent, and Live

Rachid Guerraoui, Victor Bushkov, Panagiota Fatourou

We establish a theorem called the PCL theorem, which states that it is impossible to design a transactional memory algorithm that ensures (1) parallelism, i.e., transactions do not need to synchronize unless they access the same application objects, (2) ve ...

ASSOC COMPUTING MACHINERY2019

Distributed Logless Atomic Durability with Persistent Memory

Babak Falsafi, Alexandros Daglis, Siddharth Gupta

Datacenter operators have started deploying Persistent Memory (PM), leveraging its combination of fast access and persistence for significant performance gains. A key challenge for PM-aware software is to maintain high performance while achieving atomic du ...

2019