Shabnam Ghasemirad


Last Name

Ghasemirad

First Name

Shabnam

ORCID

0000-0002-4193-5123

Organisational unit

03634 - Basin, David / Basin, David

Filters

2022 - 20253
Reset filters

Search Results

Publications1 - 3 of 3
  • Mechanized Data Consistency Models for Distributed Database Transactions
    Item type: Master Thesis
    Ghasemirad, Shabnam (2022)
  • Pushing the Limit: Verified Performance-Optimal Causally-Consistent Database Transactions
    Item type: Conference Paper
    Ghasemirad, Shabnam; Sprenger, Christoph; Liu, Si; et al. (2025)
    Lecture Notes in Computer Science ~ Tools and Algorithms for the Construction and Analysis of Systems
    Modern web services crucially rely on high-performance distributed databases, where concurrent transactions are isolated from each other using concurrency control protocols. Relaxed isolation levels, which permit more complex concurrent behaviors than strong levels like serializability, are used in practice for higher performance and availability. In this paper, we present Eiger-PORT+, a concurrency control protocol that achieves a strong form of causal consistency, called TCCv (Transactional Causal Consistency with convergence). We show that Eiger-PORT+ also provides performance-optimal read transactions in the presence of transactional writes, thus refuting an open conjecture that this is impossible for TCCv. We also deductively verify that Eiger-PORT+ satisfies this isolation level by refining an abstract model of transactions. This yields the first deductive verification of a complex concurrency control protocol. Furthermore, we conduct a performance evaluation showing Eiger-PORT+ ’s superior performance over the state-of-the-art.
  • VerIso: Verifiable Isolation Guarantees for Database Transactions
    Item type: Journal Article
    Ghasemirad, Shabnam; Liu, Si; Sprenger, Christoph; et al. (2025)
    Proceedings of the VLDB Endowment
    Isolation bugs, stemming especially from design-level defects, have been repeatedly found in carefully designed and extensively tested production databases over decades. In parallel, various frameworks for modeling database transactions and reasoning about their isolation guarantees have been developed. What is missing however is a mathematically rigorous and systematic framework with tool support for formally verifying a wide range of such guarantees for all possible system behaviors. We present the first such framework, VerIso, developed within the theorem prover Isabelle/HOL. To showcase its use in verification, we model the strict two-phase locking concurrency control protocol and verify that it provides strict serializability isolation guarantee. Moreover, we show how VerIso helps identify isolation bugs during protocol design. We derive new counterexamples for the TAPIR protocol from failed attempts to prove its claimed strict serializability. In particular, we show that it violates a much weaker isolation level, namely, atomic visibility.
Publications1 - 3 of 3