15 Search Results for "Jagannathan, Suresh"

Document
DOI: 10.4230/LIPIcs.ECOOP.2024.30
Verifying Lock-Free Search Structure Templates

Authors: Nisarg Patel, Dennis Shasha, and Thomas Wies

Published in: LIPIcs, Volume 313, 38th European Conference on Object-Oriented Programming (ECOOP 2024)

Abstract
We present and verify template algorithms for lock-free concurrent search structures that cover a broad range of existing implementations based on lists and skiplists. Our linearizability proofs are fully mechanized in the concurrent separation logic Iris. The proofs are modular and cover the broader design space of the underlying algorithms by parameterizing the verification over aspects such as the low-level representation of nodes and the style of data structure maintenance. As a further technical contribution, we present a mechanization of a recently proposed method for reasoning about future-dependent linearization points using hindsight arguments. The mechanization builds on Iris' support for prophecy reasoning and user-defined ghost resources. We demonstrate that the method can help to reduce the proof effort compared to direct prophecy-based proofs.
Cite as

Nisarg Patel, Dennis Shasha, and Thomas Wies. Verifying Lock-Free Search Structure Templates. In 38th European Conference on Object-Oriented Programming (ECOOP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 313, pp. 30:1-30:28, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{patel_et_al:LIPIcs.ECOOP.2024.30,
  author =	{Patel, Nisarg and Shasha, Dennis and Wies, Thomas},
  title =	{{Verifying Lock-Free Search Structure Templates}},
  booktitle =	{38th European Conference on Object-Oriented Programming (ECOOP 2024)},
  pages =	{30:1--30:28},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-341-6},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{313},
  editor =	{Aldrich, Jonathan and Salvaneschi, Guido},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2024.30},
  URN =		{urn:nbn:de:0030-drops-208797},
  doi =		{10.4230/LIPIcs.ECOOP.2024.30},
  annote =	{Keywords: skiplists, lock-free, separation logic, linearizability, future-dependent linearization points, hindsight reasoning}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2024.42
Failure Transparency in Stateful Dataflow Systems

Authors: Aleksey Veresov, Jonas Spenger, Paris Carbone, and Philipp Haller

Published in: LIPIcs, Volume 313, 38th European Conference on Object-Oriented Programming (ECOOP 2024)

Abstract
Failure transparency enables users to reason about distributed systems at a higher level of abstraction, where complex failure-handling logic is hidden. This is especially true for stateful dataflow systems, which are the backbone of many cloud applications. In particular, this paper focuses on proving failure transparency in Apache Flink, a popular stateful dataflow system. Even though failure transparency is a critical aspect of Apache Flink, to date it has not been formally proven. Showing that the failure transparency mechanism is correct, however, is challenging due to the complexity of the mechanism itself. Nevertheless, this complexity can be effectively hidden behind a failure transparent programming interface. To show that Apache Flink is failure transparent, we model it in small-step operational semantics. Next, we provide a novel definition of failure transparency based on observational explainability, a concept which relates executions according to their observations. Finally, we provide a formal proof of failure transparency for the implementation model; i.e., we prove that the failure-free model correctly abstracts from the failure-related details of the implementation model. We also show liveness of the implementation model under a fair execution assumption. These results are a first step towards a verified stack for stateful dataflow systems.
Cite as

Aleksey Veresov, Jonas Spenger, Paris Carbone, and Philipp Haller. Failure Transparency in Stateful Dataflow Systems. In 38th European Conference on Object-Oriented Programming (ECOOP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 313, pp. 42:1-42:31, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{veresov_et_al:LIPIcs.ECOOP.2024.42,
  author =	{Veresov, Aleksey and Spenger, Jonas and Carbone, Paris and Haller, Philipp},
  title =	{{Failure Transparency in Stateful Dataflow Systems}},
  booktitle =	{38th European Conference on Object-Oriented Programming (ECOOP 2024)},
  pages =	{42:1--42:31},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-341-6},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{313},
  editor =	{Aldrich, Jonathan and Salvaneschi, Guido},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2024.42},
  URN =		{urn:nbn:de:0030-drops-208911},
  doi =		{10.4230/LIPIcs.ECOOP.2024.42},
  annote =	{Keywords: Failure transparency, stateful dataflow, operational semantics, checkpoint recovery}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2024.43
Inductive Predicate Synthesis Modulo Programs

Authors: Scott Wesley, Maria Christakis, Jorge A. Navas, Richard Trefler, Valentin Wüstholz, and Arie Gurfinkel

Published in: LIPIcs, Volume 313, 38th European Conference on Object-Oriented Programming (ECOOP 2024)

Abstract
A growing trend in program analysis is to encode verification conditions within the language of the input program. This simplifies the design of analysis tools by utilizing off-the-shelf verifiers, but makes communication with the underlying solver more challenging. Essentially, the analysis tools operates at the level of input programs, whereas the solver operates at the level of problem encodings. To bridge this gap, the verifier must pass along proof-rules from the analysis tool to the solver. For example, an analysis tool for concurrent programs built on an inductive program verifier might need to declare Owicki-Gries style proof-rules for the underlying solver. Each such proof-rule further specifies how a program should be verified, meaning that the problem of passing proof-rules is a form of invariant synthesis. Similarly, many program analysis tasks reduce to the synthesis of pure, loop-free Boolean functions (i.e., predicates), relative to a program. From this observation, we propose Inductive Predicate Synthesis Modulo Programs (IPS-MP) which extends high-level languages with minimal synthesis features to guide analysis. In IPS-MP, unknown predicates appear under assume and assert statements, acting as specifications modulo the program semantics. Existing synthesis solvers are inefficient at IPS-MP as they target more general problems. In this paper, we show that IPS-MP admits an efficient solution in the Boolean case, despite being generally undecidable. Moreover, we show that IPS-MP reduces to the satisfiability of constrained Horn clauses, which is less general than existing synthesis problems, yet expressive enough to encode verification tasks. We provide reductions from challenging verification tasks - such as parameterized model checking - to IPS-MP. We realize these reductions with an efficient IPS-MP-solver based on SeaHorn, and describe a real-world application to smart-contract verification.
Cite as

Scott Wesley, Maria Christakis, Jorge A. Navas, Richard Trefler, Valentin Wüstholz, and Arie Gurfinkel. Inductive Predicate Synthesis Modulo Programs. In 38th European Conference on Object-Oriented Programming (ECOOP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 313, pp. 43:1-43:30, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{wesley_et_al:LIPIcs.ECOOP.2024.43,
  author =	{Wesley, Scott and Christakis, Maria and Navas, Jorge A. and Trefler, Richard and W\"{u}stholz, Valentin and Gurfinkel, Arie},
  title =	{{Inductive Predicate Synthesis Modulo Programs}},
  booktitle =	{38th European Conference on Object-Oriented Programming (ECOOP 2024)},
  pages =	{43:1--43:30},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-341-6},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{313},
  editor =	{Aldrich, Jonathan and Salvaneschi, Guido},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2024.43},
  URN =		{urn:nbn:de:0030-drops-208926},
  doi =		{10.4230/LIPIcs.ECOOP.2024.43},
  annote =	{Keywords: Software Verification, Invariant Synthesis, Model-Checking}
}
Document
DOI: 10.4230/LIPIcs.ITP.2024.23
A Generalised Union of Rely-Guarantee and Separation Logic Using Permission Algebras

Authors: Vincent Jackson, Toby Murray, and Christine Rizkallah

Published in: LIPIcs, Volume 309, 15th International Conference on Interactive Theorem Proving (ITP 2024)

Abstract
This paper describes GenRGSep, an Isabelle/HOL library for the development of RGSep logics using a general algebraic state model. In particular, we develop an algebraic state models based on resource algebras that assume neither the presence of unit resources or the cancellativity law. If a new resource model is required, its components need only be proven an instance of a permission algebra, and then they can be composed together using tuples and functions. The proof of soundness is performed by Vafeiadis' operational soundness method. This method was originally formulated with respect to a concrete heap model. This paper adapts it to account for the absence of both units as well as the cancellativity law.
Cite as

Vincent Jackson, Toby Murray, and Christine Rizkallah. A Generalised Union of Rely-Guarantee and Separation Logic Using Permission Algebras. In 15th International Conference on Interactive Theorem Proving (ITP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 309, pp. 23:1-23:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{jackson_et_al:LIPIcs.ITP.2024.23,
  author =	{Jackson, Vincent and Murray, Toby and Rizkallah, Christine},
  title =	{{A Generalised Union of Rely-Guarantee and Separation Logic Using Permission Algebras}},
  booktitle =	{15th International Conference on Interactive Theorem Proving (ITP 2024)},
  pages =	{23:1--23:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-337-9},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{309},
  editor =	{Bertot, Yves and Kutsia, Temur and Norrish, Michael},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2024.23},
  URN =		{urn:nbn:de:0030-drops-207510},
  doi =		{10.4230/LIPIcs.ITP.2024.23},
  annote =	{Keywords: verification, concurrency, rely-guarantee, separation logic, resource algebras}
}
Document
DOI: 10.4230/LIPIcs.ITP.2024.36
Defining and Preserving More C Behaviors: Verified Compilation Using a Concrete Memory Model

Authors: Andrew Tolmach, Chris Chhak, and Sean Anderson

Published in: LIPIcs, Volume 309, 15th International Conference on Interactive Theorem Proving (ITP 2024)

Abstract
We propose a concrete ("pointer as integer") memory semantics for C that supports verified compilation to a target environment having simple "public vs. private" data protection based on tagging or sandboxing (such as the WebAssembly virtual machine). Our semantics gives definition to a range of legacy programming idioms that cause undefined behavior in standard C, and are not covered by existing verified compilers, but that often work in practice. Compiler correctness in this context implies that target programs are secure against all control-flow attacks (although not against data-only attacks). To avoid tying our semantics too closely to particular compiler implementation choices, it is parameterized by a novel form of oracle that non-deterministically chooses the addresses of stack and heap allocations. As a proof-of-concept, we formalize a small RTL-like language and verify two-way refinement for a compiler from this language to a low-level machine and runtime system with hardware tagging. Our Coq formalization and proofs are provided as supplementary material.
Cite as

Andrew Tolmach, Chris Chhak, and Sean Anderson. Defining and Preserving More C Behaviors: Verified Compilation Using a Concrete Memory Model. In 15th International Conference on Interactive Theorem Proving (ITP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 309, pp. 36:1-36:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{tolmach_et_al:LIPIcs.ITP.2024.36,
  author =	{Tolmach, Andrew and Chhak, Chris and Anderson, Sean},
  title =	{{Defining and Preserving More C Behaviors: Verified Compilation Using a Concrete Memory Model}},
  booktitle =	{15th International Conference on Interactive Theorem Proving (ITP 2024)},
  pages =	{36:1--36:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-337-9},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{309},
  editor =	{Bertot, Yves and Kutsia, Temur and Norrish, Michael},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2024.36},
  URN =		{urn:nbn:de:0030-drops-207643},
  doi =		{10.4230/LIPIcs.ITP.2024.36},
  annote =	{Keywords: Compiler verification, C language semantics, Coq proof assistant}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2024.33
Automating Memory Model Metatheory with Intersections

Authors: Aristotelis Koutsouridis, Michalis Kokologiannakis, and Viktor Vafeiadis

Published in: LIPIcs, Volume 311, 35th International Conference on Concurrency Theory (CONCUR 2024)

Abstract
In the weak memory consistency literature, the semantics of concurrent programs is typically defined as a constraint on execution graphs, expressed in relational algebra. Prior work has shown that basic metatheoretic questions about memory models are decidable as long as they can be expressed as irreflexivity and emptiness constraints over Kleene Algebra with Tests (KAT), a condition that rules out practical memory models such the C/C++ and the Linux kernel models. In this paper, we extend these results to memory models containing arbitrary intersections with uninterpreted relations. We can thus automatically establish compilation correctness and derive efficient incremental consistency checkers for RC11, LKMM, and other memory models.
Cite as

Aristotelis Koutsouridis, Michalis Kokologiannakis, and Viktor Vafeiadis. Automating Memory Model Metatheory with Intersections. In 35th International Conference on Concurrency Theory (CONCUR 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 311, pp. 33:1-33:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{koutsouridis_et_al:LIPIcs.CONCUR.2024.33,
  author =	{Koutsouridis, Aristotelis and Kokologiannakis, Michalis and Vafeiadis, Viktor},
  title =	{{Automating Memory Model Metatheory with Intersections}},
  booktitle =	{35th International Conference on Concurrency Theory (CONCUR 2024)},
  pages =	{33:1--33:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-339-3},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{311},
  editor =	{Majumdar, Rupak and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2024.33},
  URN =		{urn:nbn:de:0030-drops-208050},
  doi =		{10.4230/LIPIcs.CONCUR.2024.33},
  annote =	{Keywords: Kleene Algebra, Weak Memory Models}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2024.23
Mirroring Call-By-Need, or Values Acting Silly

Authors: Beniamino Accattoli and Adrienne Lancelot

Published in: LIPIcs, Volume 299, 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)

Abstract
Call-by-need evaluation for the λ-calculus can be seen as merging the best of call-by-name and call-by-value, namely the wise erasing behaviour of the former and the wise duplicating behaviour of the latter. To better understand how duplication and erasure can be combined, we design a degenerated calculus, dubbed call-by-silly, that is symmetric to call-by-need in that it merges the worst of call-by-name and call-by-value, namely silly duplications by-name and silly erasures by-value. We validate the design of the call-by-silly calculus via rewriting properties and multi types. In particular, we mirror the main theorem about call-by-need - that is, its operational equivalence with call-by-name - showing that call-by-silly and call-by-value induce the same contextual equivalence. This fact shows the blindness with respect to efficiency of call-by-value contextual equivalence. We also define a call-by-silly strategy and measure its length via tight multi types. Lastly, we prove that the call-by-silly strategy computes evaluation sequences of maximal length in the calculus.
Cite as

Beniamino Accattoli and Adrienne Lancelot. Mirroring Call-By-Need, or Values Acting Silly. In 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 299, pp. 23:1-23:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{accattoli_et_al:LIPIcs.FSCD.2024.23,
  author =	{Accattoli, Beniamino and Lancelot, Adrienne},
  title =	{{Mirroring Call-By-Need, or Values Acting Silly}},
  booktitle =	{9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)},
  pages =	{23:1--23:24},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-323-2},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{299},
  editor =	{Rehof, Jakob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2024.23},
  URN =		{urn:nbn:de:0030-drops-203527},
  doi =		{10.4230/LIPIcs.FSCD.2024.23},
  annote =	{Keywords: Lambda calculus, intersection types, call-by-value, call-by-need}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2024.24
IMELL Cut Elimination with Linear Overhead

Authors: Beniamino Accattoli and Claudio Sacerdoti Coen

Published in: LIPIcs, Volume 299, 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)

Abstract
Recently, Accattoli introduced the Exponential Substitution Calculus (ESC) given by untyped proof terms for Intuitionistic Multiplicative Exponential Linear Logic (IMELL), endowed with rewriting rules at-a-distance for cut elimination. He also introduced a new cut elimination strategy, dubbed the good strategy, and showed that its number of steps is a time cost model with polynomial overhead for ESC/IMELL, and the first such one. Here, we refine Accattoli’s result by introducing an abstract machine for ESC and proving that it implements the good strategy and computes cut-free terms/proofs within a linear overhead.
Cite as

Beniamino Accattoli and Claudio Sacerdoti Coen. IMELL Cut Elimination with Linear Overhead. In 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 299, pp. 24:1-24:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{accattoli_et_al:LIPIcs.FSCD.2024.24,
  author =	{Accattoli, Beniamino and Sacerdoti Coen, Claudio},
  title =	{{IMELL Cut Elimination with Linear Overhead}},
  booktitle =	{9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)},
  pages =	{24:1--24:24},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-323-2},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{299},
  editor =	{Rehof, Jakob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2024.24},
  URN =		{urn:nbn:de:0030-drops-203539},
  doi =		{10.4230/LIPIcs.FSCD.2024.24},
  annote =	{Keywords: Lambda calculus, linear logic, abstract machines}
}
Document
Invited Talk
DOI: 10.4230/LIPIcs.FSCD.2024.1
Meaningfulness and Genericity in a Subsuming Framework (Invited Talk)

Authors: Delia Kesner, Victor Arrial, and Giulio Guerrieri

Published in: LIPIcs, Volume 299, 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)

Abstract
This paper studies the notion of meaningfulness for a unifying framework called dBang-calculus, which subsumes both call-by-name (dCBN) and call-by-value (dCBV). We first define meaningfulness in dBang and then characterize it by means of typability and inhabitation in an associated non-idempotent intersection type system previously appearing in the literature. We validate the proposed notion of meaningfulness by showing two properties: (1) consistency of the smallest theory, called ℋ, equating all meaningless terms, and (2) genericity, stating that meaningless subterms have no bearing on the significance of meaningful terms. The theory ℋ is also shown to have a unique consistent and maximal extension ℋ*, which coincides with a well-known notion of observational equivalence. Last but not least, we show that the notions of meaningfulness and genericity in the literature for dCBN and dCBV are subsumed by the corresponding ones proposed here for the dBang-calculus.
Cite as

Delia Kesner, Delia Kesner, Victor Arrial, Victor Arrial, Giulio Guerrieri, and Giulio Guerrieri. Meaningfulness and Genericity in a Subsuming Framework (Invited Talk). In 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 299, pp. 1:1-1:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{kesner_et_al:LIPIcs.FSCD.2024.1,
  author =	{Kesner, Delia and Arrial, Victor and Guerrieri, Giulio},
  title =	{{Meaningfulness and Genericity in a Subsuming Framework}},
  booktitle =	{9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)},
  pages =	{1:1--1:24},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-323-2},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{299},
  editor =	{Rehof, Jakob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2024.1},
  URN =		{urn:nbn:de:0030-drops-203305},
  doi =		{10.4230/LIPIcs.FSCD.2024.1},
  annote =	{Keywords: Lambda calculus, Solvability, Meaningfulness, Inhabitation, Genericity}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2023.20
Morpheus: Automated Safety Verification of Data-Dependent Parser Combinator Programs

Authors: Ashish Mishra and Suresh Jagannathan

Published in: LIPIcs, Volume 263, 37th European Conference on Object-Oriented Programming (ECOOP 2023)

Abstract
Parser combinators are a well-known mechanism used for the compositional construction of parsers, and have shown to be particularly useful in writing parsers for rich grammars with data-dependencies and global state. Verifying applications written using them, however, has proven to be challenging in large part because of the inherently effectful nature of the parsers being composed and the difficulty in reasoning about the arbitrarily rich data-dependent semantic actions that can be associated with parsing actions. In this paper, we address these challenges by defining a parser combinator framework called Morpheus equipped with abstractions for defining composable effects tailored for parsing and semantic actions, and a rich specification language used to define safety properties over the constituent parsers comprising a program. Even though its abstractions yield many of the same expressivity benefits as other parser combinator systems, Morpheus is carefully engineered to yield a substantially more tractable automated verification pathway. We demonstrate its utility in verifying a number of realistic, challenging parsing applications, including several cases that involve non-trivial data-dependent relations.
Cite as

Ashish Mishra and Suresh Jagannathan. Morpheus: Automated Safety Verification of Data-Dependent Parser Combinator Programs. In 37th European Conference on Object-Oriented Programming (ECOOP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 263, pp. 20:1-20:27, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{mishra_et_al:LIPIcs.ECOOP.2023.20,
  author =	{Mishra, Ashish and Jagannathan, Suresh},
  title =	{{Morpheus: Automated Safety Verification of Data-Dependent Parser Combinator Programs}},
  booktitle =	{37th European Conference on Object-Oriented Programming (ECOOP 2023)},
  pages =	{20:1--20:27},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-281-5},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{263},
  editor =	{Ali, Karim and Salvaneschi, Guido},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2023.20},
  URN =		{urn:nbn:de:0030-drops-182138},
  doi =		{10.4230/LIPIcs.ECOOP.2023.20},
  annote =	{Keywords: Parsers, Verification, Domain-specific languages, Functional programming, Refinement types, Type systems}
}
Document
DOI: 10.4230/LIPIcs.SNAPL.2019.8
Version Control Is for Your Data Too

Authors: Gowtham Kaki, KC Sivaramakrishnan, and Suresh Jagannathan

Published in: LIPIcs, Volume 136, 3rd Summit on Advances in Programming Languages (SNAPL 2019)

Abstract
Programmers regularly use distributed version control systems (DVCS) such as Git to facilitate collaborative software development. The primary purpose of a DVCS is to maintain integrity of source code in the presence of concurrent, possibly conflicting edits from collaborators. In addition to safely merging concurrent non-conflicting edits, a DVCS extensively tracks source code provenance to help programmers contextualize and resolve conflicts. Provenance also facilitates debugging by letting programmers see diffs between versions and quickly find those edits that introduced the offending conflict (e.g., via git blame). In this paper, we posit that analogous workflows to collaborative software development also arise in distributed software execution; we argue that the characteristics that make a DVCS an ideal fit for the former also make it an ideal fit for the latter. Building on this observation, we propose a distributed programming model, called carmot that views distributed shared state as an entity evolving in time, manifested as a sequence of persistent versions, and relies on an explicitly defined merge semantics to reconcile concurrent conflicting versions. We show examples demonstrating how carmot simplifies distributed programming, while also enabling novel workflows integral to modern applications such as blockchains. We also describe a prototype implementation of carmot that we use to evaluate its practicality.
Cite as

Gowtham Kaki, KC Sivaramakrishnan, and Suresh Jagannathan. Version Control Is for Your Data Too. In 3rd Summit on Advances in Programming Languages (SNAPL 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 136, pp. 8:1-8:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{kaki_et_al:LIPIcs.SNAPL.2019.8,
  author =	{Kaki, Gowtham and Sivaramakrishnan, KC and Jagannathan, Suresh},
  title =	{{Version Control Is for Your Data Too}},
  booktitle =	{3rd Summit on Advances in Programming Languages (SNAPL 2019)},
  pages =	{8:1--8:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-113-9},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{136},
  editor =	{Lerner, Benjamin S. and Bod{\'\i}k, Rastislav and Krishnamurthi, Shriram},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SNAPL.2019.8},
  URN =		{urn:nbn:de:0030-drops-105516},
  doi =		{10.4230/LIPIcs.SNAPL.2019.8},
  annote =	{Keywords: replication, distributed systems, version control}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2018.41
Automated Detection of Serializability Violations Under Weak Consistency

Authors: Kartik Nagar and Suresh Jagannathan

Published in: LIPIcs, Volume 118, 29th International Conference on Concurrency Theory (CONCUR 2018)

Abstract
While a number of weak consistency mechanisms have been developed in recent years to improve performance and ensure availability in distributed, replicated systems, ensuring the correctness of transactional applications running on top of such systems remains a difficult and important problem. Serializability is a well-understood correctness criterion for transactional programs; understanding whether applications are serializable when executed in a weakly-consistent environment, however remains a challenging exercise. In this work, we combine a dependency graph-based characterization of serializability and leverage the framework of abstract executions to develop a fully-automated approach for statically finding bounded serializability violations under any weak consistency model. We reduce the problem of serializability to satisfiability of a formula in First-Order Logic (FOL), which allows us to harness the power of existing SMT solvers. We provide rules to automatically construct the FOL encoding from programs written in SQL (allowing loops and conditionals) and express consistency specifications as FOL formula. In addition to detecting bounded serializability violations, we also provide two orthogonal schemes to reason about unbounded executions by providing sufficient conditions (again, in the form of FOL formulae) whose satisfiability implies the absence of anomalies in any arbitrary execution. We have applied the proposed technique on TPC-C, a real-world database program with complex application logic, and were able to discover anomalies under Parallel Snapshot Isolation (PSI), and verify serializability for unbounded executions under Snapshot Isolation (SI), two consistency mechanisms substantially weaker than serializability.
Cite as

Kartik Nagar and Suresh Jagannathan. Automated Detection of Serializability Violations Under Weak Consistency. In 29th International Conference on Concurrency Theory (CONCUR 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 118, pp. 41:1-41:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{nagar_et_al:LIPIcs.CONCUR.2018.41,
  author =	{Nagar, Kartik and Jagannathan, Suresh},
  title =	{{Automated Detection of Serializability Violations Under Weak Consistency}},
  booktitle =	{29th International Conference on Concurrency Theory (CONCUR 2018)},
  pages =	{41:1--41:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-087-3},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{118},
  editor =	{Schewe, Sven and Zhang, Lijun},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2018.41},
  URN =		{urn:nbn:de:0030-drops-95799},
  doi =		{10.4230/LIPIcs.CONCUR.2018.41},
  annote =	{Keywords: Weak Consistency, Serializability, Database Applications}
}
Document
DOI: 10.4230/DagRep.6.3.59
Language Based Verification Tools for Functional Programs (Dagstuhl Seminar 16131)

Authors: Marco Gaboardi, Suresh Jagannathan, Ranjit Jhala, and Stephanie Weirich

Published in: Dagstuhl Reports, Volume 6, Issue 3 (2016)

Abstract
This report documents the program and the outcomes of Dagstuhl Seminar 16131 "Language Based Verification Tools for Functional Programs". This seminar is motivated by two converging trends in computing -- the increasing reliance on software has led to an increased interest in seeking formal, reliable means of ensuring that programs possess crucial correctness properties, and the dramatic increase in adoption of higher-order functional languages due to the web, multicore and "big data" revolutions. While the research community has studied the problem of language based verification for imperative and first-order programs for decades – yielding important ideas like Floyd-Hoare Logics, Abstract Interpretation, Model Checking, and Separation Logic and so on – it is only relatively recently, that proposals have emerged for language baseverification tools for functional and higher-order programs. These techniques include advanced type systems, contract systems, model checking and program analyses specially tailored to exploit the structure of functional languages. These proposals are from groups based in diverse research communities, attacking the problem from different angles, yielding techniques with complementary strengths. This seminar brought diverse set of researchers together so that we could: compare the strengths and limitations of different approaches, discuss ways to unify the complementary advantages of different techniques, both conceptually and in tools, share challenging open problems and application areas where verification may be most effective, identify novel ways of using verification techniques for other software engineering tasks such as code search or synthesis, and improve the pedagogy and hence adoption of such techniques.
Cite as

Marco Gaboardi, Suresh Jagannathan, Ranjit Jhala, and Stephanie Weirich. Language Based Verification Tools for Functional Programs (Dagstuhl Seminar 16131). In Dagstuhl Reports, Volume 6, Issue 3, pp. 59-77, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@Article{gaboardi_et_al:DagRep.6.3.59,
  author =	{Gaboardi, Marco and Jagannathan, Suresh and Jhala, Ranjit and Weirich, Stephanie},
  title =	{{Language Based Verification Tools for Functional Programs (Dagstuhl Seminar 16131)}},
  pages =	{59--77},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2016},
  volume =	{6},
  number =	{3},
  editor =	{Gaboardi, Marco and Jagannathan, Suresh and Jhala, Ranjit and Weirich, Stephanie},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.6.3.59},
  URN =		{urn:nbn:de:0030-drops-61494},
  doi =		{10.4230/DagRep.6.3.59},
  annote =	{Keywords: Functional Programming, Type Systems, Contracts, Dependent Types, Model Checking, Program Analysis}
}
Document
Invited Talk
DOI: 10.4230/LIPIcs.FSTTCS.2015.9
Relational Refinement Types for Higher-Order Shape Transformers (Invited Talk)

Authors: Suresh Jagannathan

Published in: LIPIcs, Volume 45, 35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015)

Abstract
Understanding, discovering, and proving useful properties of sophisticated data structures are central problems in program verification. A particularly challenging exercise for shape analyses involves reasoning about sophisticated shape transformers that preserve the shape of a data structure (e.g., the data structure skeleton is always maintained as a balanced tree) or the relationship among values contained therein (e.g., the in-order relation of the elements of a tree or the parent-child relation of the elements of a heap) across program transformations. In this talk, we consider the specification and verification of such transformers for ML programs. The structural properties preserved by transformers can often be naturally expressed as inductively-defined relations over the recursive structure evident in the definitions of the datatypes they manipulate. By carefully augmenting a refinement type system with support for reasoning about structural relations over algebraic datatypes, we realize an expressive yet decidable specification language, capable of capturing useful structural invariants, which can nonetheless be automatically verified using off-the-shelf type checkers and theorem provers. Notably, our technique generalizes to definitions of parametric relations for polymorphic data types which, in turn, lead to highly composable specifications over higher-order polymorphic shape transformers.
Cite as

Suresh Jagannathan. Relational Refinement Types for Higher-Order Shape Transformers (Invited Talk). In 35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 45, p. 9, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{jagannathan:LIPIcs.FSTTCS.2015.9,
  author =	{Jagannathan, Suresh},
  title =	{{Relational Refinement Types for Higher-Order Shape Transformers}},
  booktitle =	{35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015)},
  pages =	{9--9},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-97-2},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{45},
  editor =	{Harsha, Prahladh and Ramalingam, G.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2015.9},
  URN =		{urn:nbn:de:0030-drops-56406},
  doi =		{10.4230/LIPIcs.FSTTCS.2015.9},
  annote =	{Keywords: Relational Specifications; Inductive and Parametric Relations; Refinement Types, Shape Analysis, Data Structure Verification\}}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2015.445
Cooking the Books: Formalizing JMM Implementation Recipes

Authors: Gustavo Petri, Jan Vitek, and Suresh Jagannathan

Published in: LIPIcs, Volume 37, 29th European Conference on Object-Oriented Programming (ECOOP 2015)

Abstract
The Java Memory Model (JMM) is intended to characterize the meaning of concurrent Java programs. Because of the model's complexity, however, its definition cannot be easily transplanted within an optimizing Java compiler, even though an important rationale for its design was to ensure Java compiler optimizations are not unduly hampered because of the language's concurrency features. In response, Lea's JSR-133 Cookbook for Compiler Writers, an informal guide to realizing the principles underlying the JMM on different (relaxed-memory) platforms was developed. The goal of the cookbook is to give compiler writers a relatively simple, yet reasonably efficient, set of reordering-based recipes that satisfy JMM constraints. In this paper, we present the first formalization of the cookbook, providing a semantic basis upon which the relationship between the recipes defined by the cookbook and the guarantees enforced by the JMM can be rigorously established. Notably, one artifact of our investigation is that the rules defined by the cookbook for compiling Java onto Power are inconsistent with the requirements of the JMM, a surprising result, and one which justifies our belief in the need for formally provable definitions to reason about sophisticated (and racy) concurrency patterns in Java, and their implementation on modern-day relaxed-memory hardware. Our formalization enables simulation arguments between an architecture-independent intermediate representation of the kind suggested by Lea with machine abstractions for Power and x86. Moreover, we provide fixes for cookbook recipes that are inconsistent with the behaviors admitted by the target platform, and prove the correctness of these repairs.
Cite as

Gustavo Petri, Jan Vitek, and Suresh Jagannathan. Cooking the Books: Formalizing JMM Implementation Recipes. In 29th European Conference on Object-Oriented Programming (ECOOP 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 37, pp. 445-469, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{petri_et_al:LIPIcs.ECOOP.2015.445,
  author =	{Petri, Gustavo and Vitek, Jan and Jagannathan, Suresh},
  title =	{{Cooking the Books: Formalizing JMM Implementation Recipes}},
  booktitle =	{29th European Conference on Object-Oriented Programming (ECOOP 2015)},
  pages =	{445--469},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-86-6},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{37},
  editor =	{Boyland, John Tang},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2015.445},
  URN =		{urn:nbn:de:0030-drops-52334},
  doi =		{10.4230/LIPIcs.ECOOP.2015.445},
  annote =	{Keywords: Concurrency, Java, Memory Model, Relaxed-Memory}
}
  • Refine by Author
  • 6 Jagannathan, Suresh
  • 2 Accattoli, Beniamino
  • 1 Anderson, Sean
  • 1 Arrial, Victor
  • 1 Carbone, Paris
  • Show More...

  • Refine by Classification
  • 3 Theory of computation → Logic and verification
  • 3 Theory of computation → Operational semantics
  • 2 Theory of computation → Concurrency
  • 2 Theory of computation → Separation logic
  • 1 Computing methodologies → Distributed programming languages
  • Show More...

  • Refine by Keyword
  • 3 Lambda calculus
  • 2 separation logic
  • 1 C language semantics
  • 1 Compiler verification
  • 1 Concurrency
  • Show More...

  • Refine by Type
  • 15 document

  • Refine by Publication Year
  • 9 2024
  • 2 2015
  • 1 2016
  • 1 2018
  • 1 2019
  • Show More...

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