Showing 1–33 of 33 results for author: Thiemann, P

Partial Orders for Precise and Efficient Dynamic Deadlock Prediction

Authors: Bas van den Heuvel, Martin Sulzmann, Peter Thiemann

Abstract: Deadlocks are a major source of bugs in concurrent programs. They are hard to predict, because they may only occur under specific scheduling conditions. Dynamic analysis attempts to identify potential deadlocks by examining a single execution trace of the program. A standard approach involves monitoring sequences of lock acquisitions in each thread, with the goal of identifying deadlock patterns.… ▽ More Deadlocks are a major source of bugs in concurrent programs. They are hard to predict, because they may only occur under specific scheduling conditions. Dynamic analysis attempts to identify potential deadlocks by examining a single execution trace of the program. A standard approach involves monitoring sequences of lock acquisitions in each thread, with the goal of identifying deadlock patterns. A deadlock pattern is characterized by a cyclic chain of lock acquisitions, where each lock is held by one thread while being requested by the next. However, it is well known that not all deadlock patterns identified in this way correspond to true deadlocks, as they may be impossible to manifest under any schedule. We tackle this deficiency by proposing a new method based on partial orders to eliminate false positives: lock acquisitions must be unordered under a given partial order, and not preceded by other deadlock patterns. We prove soundness (no falsely predicted deadlocks) for the novel TRW partial order, and completeness (no deadlocks missed) for a slightly weakened variant of TRW. Both partial orders can be computed efficiently and report the same deadlocks for an extensive benchmark suite. △ Less

Submitted 27 February, 2025; originally announced February 2025.

Law and Order for Typestate with Borrowing

Authors: Hannes Saffrich, Yuki Nishida, Peter Thiemann

Abstract: Typestate systems are notoriously complex as they require sophisticated machinery for tracking aliasing. We propose a new, transition-oriented foundation for typestate in the setting of impure functional programming. Our approach relies on ordered types for simple alias tracking and its formalization draws on work on bunched implications. Yet, we support a flexible notion of borrowing in the prese… ▽ More Typestate systems are notoriously complex as they require sophisticated machinery for tracking aliasing. We propose a new, transition-oriented foundation for typestate in the setting of impure functional programming. Our approach relies on ordered types for simple alias tracking and its formalization draws on work on bunched implications. Yet, we support a flexible notion of borrowing in the presence of typestate. Our core calculus comes with a notion of resource types indexed by an ordered partial monoid that models abstract state transitions. We prove syntactic type soundness with respect to a resource-instrumented semantics. We give an algorithmic version of our type system and prove its soundness. Algorithmic typing facilitates a simple surface language that does not expose tedious details of ordered types. We implemented a typechecker for the surface language along with an interpreter for the core language. △ Less

Submitted 25 September, 2024; v1 submitted 26 August, 2024; originally announced August 2024.

Cross-thread critical sections and efficient dynamic race prediction methods

Authors: Martin Sulzmann, Peter Thiemann

Abstract: The lock set method and the partial order method are two main approaches to guarantee that dynamic data race prediction remains efficient. There are many variations of these ideas. Common to all of them is the assumption that the events in a critical section belong to the same thread. We have evidence that critical sections in the wild do extend across thread boundaries even if the surrounding a… ▽ More The lock set method and the partial order method are two main approaches to guarantee that dynamic data race prediction remains efficient. There are many variations of these ideas. Common to all of them is the assumption that the events in a critical section belong to the same thread. We have evidence that critical sections in the wild do extend across thread boundaries even if the surrounding acquire and release events occur in the same thread. We introduce the novel concept of a cross-thread critical section to capture such situations, offer a theoretical comprehensive framework, and study their impact on state-of-the-art data race analyses. For the sound partial order relation WCP we can show that the soundness claim also applies to cross-thread critical sections. For DCtp the occurrence of cross-thread critical sections invalidates the soundness claim. For complete partial order relations such as WDP and PWR, cross-thread critical sections help to eliminate more false positives. The same (positive) impact applies to the lock set construction. Our experimental evaluation confirms that cross-thread critical sections arise in practice. For the complete relation PWR, we are able to reduce the number of false positives. The performance overhead incurred by tracking cross-thread critical sections slows down the analysis by 10%-20%, on average. △ Less

Submitted 12 October, 2023; v1 submitted 19 July, 2023; originally announced July 2023.

Comments: Revised POPL'24 submission. 1. WCP is sound and show that WCP soundness proof can be adapted. 2. Cross-thread critical sections arise in practice, though the impact is not drastic. This in line with other works (like WCP) that advance the state of the art

Parameterized Algebraic Protocols

Authors: Andreia Mordido, Janek Spaderna, Peter Thiemann, Vasco T. Vasconcelos

Abstract: We propose algebraic protocols that enable the definition of protocol templates and session types analogous to the definition of domain-specific types with algebraic datatypes. Parameterized algebraic protocols subsume all regular as well as most context-free and nested session types and, at the same time, replace the expensive superlinear algorithms for type checking by a nominal check that runs… ▽ More We propose algebraic protocols that enable the definition of protocol templates and session types analogous to the definition of domain-specific types with algebraic datatypes. Parameterized algebraic protocols subsume all regular as well as most context-free and nested session types and, at the same time, replace the expensive superlinear algorithms for type checking by a nominal check that runs in linear time. Algebraic protocols in combination with polymorphism increase expressiveness and modularity by facilitating new ways of parameterizing and composing session types. △ Less

Submitted 7 April, 2023; originally announced April 2023.

ACM Class: D.3.1

Intrinsically Typed Sessions With Callbacks

Authors: Peter Thiemann

Abstract: All formalizations of session types rely on linear types for soundness as session-typed communication channels must change their type at every operation. Embedded language implementations of session types follow suit. They either rely on clever typing constructions to guarantee linearity statically, or on run-time checks that approximate linearity. We present a new language embedded implementati… ▽ More All formalizations of session types rely on linear types for soundness as session-typed communication channels must change their type at every operation. Embedded language implementations of session types follow suit. They either rely on clever typing constructions to guarantee linearity statically, or on run-time checks that approximate linearity. We present a new language embedded implementation of session types, which is inspired by the inversion of control design principle. With our approach, all application programs are intrinsically session typed and unable to break linearity by construction. Linearity remains a proof obligation for a tiny encapsulated library that can be discharged once and for all when the library is built. We demonstrate that our proposed design extends to a wide range of features of session type systems: branching, recursion, multichannel and higher-order session, as well as context-free sessions. The multichannel extension provides an embedded implementation of session types which guarantees deadlock freedom by construction. The development reported in this paper is fully backed by type-checked Agda code. △ Less

Submitted 2 March, 2023; originally announced March 2023.

Comments: 27 pages; in submission

MSC Class: 68N18 ACM Class: D.1.1; D.3.3; F.3.3

Polymorphic Typestate for Session Types

Authors: Hannes Saffrich, Peter Thiemann

Abstract: Session types provide a principled approach to typed communication protocols that guarantee type safety and protocol fidelity. Formalizations of session-typed communication are typically based on process calculi, concurrent lambda calculi, or linear logic. An alternative model based on context-sensitive typing and typestate has not received much attention due to its apparent restrictions. However,… ▽ More Session types provide a principled approach to typed communication protocols that guarantee type safety and protocol fidelity. Formalizations of session-typed communication are typically based on process calculi, concurrent lambda calculi, or linear logic. An alternative model based on context-sensitive typing and typestate has not received much attention due to its apparent restrictions. However, this model is attractive because it does not force programmers into particular patterns like continuation-passing style or channel-passing style, but rather enables them to treat communication channels like mutable variables. Polymorphic typestate is the key that enables a full treatment of session-typed communication. Previous work in this direction was hampered by its setting in a simply-typed lambda calculus. We show that higher-order polymorphism and existential types enable us to lift the restrictions imposed by the previous work, thus bringing the expressivity of the typestate-based approach on par with the competition. On this basis, we define PolyVGR, the system of polymorphic typestate for session types, establish its basic metatheory, type preservation and progress, and present a prototype implementation. △ Less

Submitted 14 August, 2023; v1 submitted 31 October, 2022; originally announced October 2022.

Comments: 29 pages. Short version appears in PPDP 2023

MSC Class: 68N15 ACM Class: D.3.1; D.3.3

Global Type Inference for Featherweight Generic Java

Authors: Andreas Stadelmeier, Martin Plümicke, Peter Thiemann

Abstract: Java's type system mostly relies on type checking augmented with local type inference to improve programmer convenience. We study global type inference for Featherweight Generic Java (FGJ), a functional Java core language. Given generic class headers and field specifications, our inference algorithm infers all method types if classes do not make use of polymorphic recursion. The algorithm is const… ▽ More Java's type system mostly relies on type checking augmented with local type inference to improve programmer convenience. We study global type inference for Featherweight Generic Java (FGJ), a functional Java core language. Given generic class headers and field specifications, our inference algorithm infers all method types if classes do not make use of polymorphic recursion. The algorithm is constraint-based and improves on prior work in several respects. Despite the restricted setting, global type inference for FGJ is NP-complete. △ Less

Submitted 19 May, 2022; v1 submitted 18 May, 2022; originally announced May 2022.

Comments: 33 pages, abridged version appears in ECOOP 2022

MSC Class: 68N15 ACM Class: D.3.1; F.3.3

A Typed Programmatic Interface to Contracts on the Blockchain

Authors: Thi Thu Ha Doan, Peter Thiemann

Abstract: Smart contract applications on the blockchain can only reach their full potential if they integrate seamlessly with traditional software systems via a programmatic interface. This interface should provide for originating and invoking contracts as well as observing the state of the blockchain. We propose a typed API for this purpose and establish some properties of the combined system. Specifically… ▽ More Smart contract applications on the blockchain can only reach their full potential if they integrate seamlessly with traditional software systems via a programmatic interface. This interface should provide for originating and invoking contracts as well as observing the state of the blockchain. We propose a typed API for this purpose and establish some properties of the combined system. Specifically, we provide an execution model that enables us to prove type-safe interaction between programs and the blockchain. We establish further properties of the model that give rise to requirements on the API. A prototype of the interface is implemented in OCaml for the Tezos blockchain. △ Less

Submitted 29 August, 2021; v1 submitted 26 August, 2021; originally announced August 2021.

Comments: 19 pages + 8 pages appendix. Appears in APLAS 2021. Extended version with proofs in appendix

MSC Class: 68N15

Generation of TypeScript Declaration Files from JavaScript Code

Authors: Fernando Cristiani, Peter Thiemann

Abstract: Developers are starting to write large and complex applications in TypeScript, a typed dialect of JavaScript. TypeScript applications integrate JavaScript libraries via typed descriptions of their APIs called declaration files. DefinitelyTyped is the standard public repository for these files. The repository is populated and maintained manually by volunteers, which is error-prone and time consumin… ▽ More Developers are starting to write large and complex applications in TypeScript, a typed dialect of JavaScript. TypeScript applications integrate JavaScript libraries via typed descriptions of their APIs called declaration files. DefinitelyTyped is the standard public repository for these files. The repository is populated and maintained manually by volunteers, which is error-prone and time consuming. Discrepancies between a declaration file and the JavaScript implementation lead to incorrect feedback from the TypeScript IDE and, thus, to incorrect uses of the underlying JavaScript library. This work presents dts-generate, a tool that generates TypeScript declaration files for JavaScript libraries uploaded to the NPM registry. It extracts code examples from the documentation written by the developer, executes the library driven by the examples, gathers run-time information, and generates a declaration file based on this information. To evaluate the tool, 249 declaration files were generated directly from an NPM module and 111 of these were compared with the corresponding declaration file provided on DefinitelyTyped. All these files either exhibited no differences at all or differences that can be resolved by extending the developer-provided examples. △ Less

Submitted 18 August, 2021; originally announced August 2021.

Comments: Appears in MPLR 2021

MSC Class: 68N15

Polymorphic Lambda Calculus with Context-Free Session Types

Authors: Bernardo Almeida, Andreia Mordido, Peter Thiemann, Vasco T. Vasconcelos

Abstract: Context-free session types provide a typing discipline for recursive structured communication protocols on bidirectional channels. They overcome the restriction of regular session type systems to tail recursive protocols. This extension enables us to implement serialisation and deserialisation of tree structures in a fully type-safe manner. We present the theory underlying the language FreeST 2,… ▽ More Context-free session types provide a typing discipline for recursive structured communication protocols on bidirectional channels. They overcome the restriction of regular session type systems to tail recursive protocols. This extension enables us to implement serialisation and deserialisation of tree structures in a fully type-safe manner. We present the theory underlying the language FreeST 2, which features context-free session types in an extension of System F with linear types and a kind system to distinguish message types and channel types. The system presents some metatheoretical challenges, which we address, contractivity in the presence of polymorphism, a non-trivial equational theory on types, and decidability of type equivalence. We also establish standard results on type preservation, progress, and a characterisation of erroneous processes. △ Less

Submitted 2 August, 2022; v1 submitted 11 June, 2021; originally announced June 2021.

Relating Functional and Imperative Session Types

Authors: Hannes Saffrich, Peter Thiemann

Abstract: Imperative session types provide an imperative interface to session-typed communication. In such an interface, channel references are first-class objects with operations that change the typestate of the channel. Compared to functional session type APIs, the program structure is simpler at the surface, but typestate is required to model the current state of communication throughout. Following an ea… ▽ More Imperative session types provide an imperative interface to session-typed communication. In such an interface, channel references are first-class objects with operations that change the typestate of the channel. Compared to functional session type APIs, the program structure is simpler at the surface, but typestate is required to model the current state of communication throughout. Following an early work that explored the imperative approach, a significant body of work on session types has neglected the imperative approach and opts for a functional approach that uses linear types to manage channel references soundly. We demonstrate that the functional approach subsumes the early work on imperative session types by exhibiting a typing and semantics preserving translation into a system of linear functional session types. We further show that the untyped backwards translation from the functional to the imperative calculus is semantics preserving. We restrict the type system of the functional calculus such that the backwards translation becomes type preserving. Thus, we precisely capture the difference in expressiveness of the two calculi and conclude that the lack of expressiveness in the imperative calculus is largely due to restrictions imposed by its type system. △ Less

Submitted 14 September, 2022; v1 submitted 16 October, 2020; originally announced October 2020.

ACM Class: D.1.3; D.3.1; F.3.2

Journal ref: Logical Methods in Computer Science, Volume 18, Issue 3 (September 15, 2022) lmcs:8815

Duality of Session Types: The Final Cut

Authors: Simon J. Gay, Peter Thiemann, Vasco T. Vasconcelos

Abstract: Duality is a central concept in the theory of session types. Since a flaw was found in the original definition of duality for recursive types, several other definitions have been published. As their connection is not obvious, we compare the competing definitions, discuss tradeoffs, and prove some equivalences. Some of the results are mechanized in Agda. Duality is a central concept in the theory of session types. Since a flaw was found in the original definition of duality for recursive types, several other definitions have been published. As their connection is not obvious, we compare the competing definitions, discuss tradeoffs, and prove some equivalences. Some of the results are mechanized in Agda. △ Less

Submitted 2 April, 2020; originally announced April 2020.

Comments: In Proceedings PLACES 2020, arXiv:2004.01062

ACM Class: D.3.1; D.3.3; F.3.3

Journal ref: EPTCS 314, 2020, pp. 23-33

Label-Dependent Session Types

Authors: Peter Thiemann, Vasco T. Vasconcelos

Abstract: Session types have emerged as a typing discipline for communication protocols. Existing calculi with session types come equipped with many different primitives that combine communication with the introduction or elimination of the transmitted value. We present a foundational session type calculus with a lightweight operational semantics. It fully decouples communication from the introduction and… ▽ More Session types have emerged as a typing discipline for communication protocols. Existing calculi with session types come equipped with many different primitives that combine communication with the introduction or elimination of the transmitted value. We present a foundational session type calculus with a lightweight operational semantics. It fully decouples communication from the introduction and elimination of data and thus features a single communication reduction, which acts as a rendezvous between senders and receivers. We achieve this decoupling by introducing label-dependent session types, a minimalist value-dependent session type system with subtyping. The system is sufficiently powerful to simulate existing functional session type systems. Compared to such systems, label-dependent session types place fewer restrictions on the code. We further introduce primitive recursion over natural numbers at the type level, thus allowing to describe protocols whose behaviour depends on numbers exchanged in messages. An algorithmic type checking system is introduced and proved equivalent to its declarative counterpart. The new calculus showcases a novel lightweight integration of dependent types and linear typing, with has uses beyond session type systems. △ Less

Submitted 11 November, 2019; v1 submitted 2 November, 2019; originally announced November 2019.

Comments: POPL 2020

Journal ref: Proc. ACM Program. Lang. 4, POPL, Article 67 (January 2020)

Kindly Bent to Free Us

Authors: Gabriel Radanne, Hannes Saffrich, Peter Thiemann

Abstract: Systems programming often requires the manipulation of resources like file handles, network connections, or dynamically allocated memory. Programmers need to follow certain protocols to handle these resources correctly. Violating these protocols causes bugs ranging from type mismatches over data races to use-after-free errors and memory leaks. These bugs often lead to security vulnerabilities. W… ▽ More Systems programming often requires the manipulation of resources like file handles, network connections, or dynamically allocated memory. Programmers need to follow certain protocols to handle these resources correctly. Violating these protocols causes bugs ranging from type mismatches over data races to use-after-free errors and memory leaks. These bugs often lead to security vulnerabilities. While statically typed programming languages guarantee type soundness and memory safety by design, most of them do not address issues arising from improper handling of resources. An important step towards handling resources is the adoption of linear and affine types that enforce single-threaded resource usage. However, the few languages supporting such types require heavy type annotations. We present Affe, an extension of ML that manages linearity and affinity properties using kinds and constrained types. In addition Affe supports the exclusive and shared borrowing of affine resources, inspired by features of Rust. Moreover, Affe retains the defining features of the ML family: it is an impure, strict, functional expression language with complete principal type inference and type abstraction. Affe does not require any linearity annotations in expressions and supports common functional programming idioms. △ Less

Submitted 25 June, 2020; v1 submitted 26 August, 2019; originally announced August 2019.

Comments: ICFP 2020

Intrinsically-Typed Mechanized Semantics for Session Types

Authors: Peter Thiemann

Abstract: Session types have emerged as a powerful paradigm for structuring communication-based programs. They guarantee type soundness and session fidelity for concurrent programs with sophisticated communication protocols. As type soundness proofs for languages with session types are tedious and technically involved, it is rare to see mechanized soundness proofs for these systems. We present an executab… ▽ More Session types have emerged as a powerful paradigm for structuring communication-based programs. They guarantee type soundness and session fidelity for concurrent programs with sophisticated communication protocols. As type soundness proofs for languages with session types are tedious and technically involved, it is rare to see mechanized soundness proofs for these systems. We present an executable intrinsically typed small-step semantics for a realistic functional session type calculus. The calculus includes linearity, recursion, and recursive sessions with subtyping. Asynchronous communication is modeled with an encoding. The semantics is implemented in Agda as an intrinsically typed, interruptible CEK machine. This implementation proves type preservation and a particular notion of progress by construction. △ Less

Submitted 8 August, 2019; originally announced August 2019.

Comments: Appears in PPDP 2019

Gradual Session Types

Authors: Atsushi Igarashi, Peter Thiemann, Yuya Tsuda, Vasco T. Vasconcelos, Philip Wadler

Abstract: Session types are a rich type discipline, based on linear types, that lifts the sort of safety claims that come with type systems to communications. However, web-based applications and microservices are often written in a mix of languages, with type disciplines in a spectrum between static and dynamic typing. Gradual session types address this mixed setting by providing a framework which grants se… ▽ More Session types are a rich type discipline, based on linear types, that lifts the sort of safety claims that come with type systems to communications. However, web-based applications and microservices are often written in a mix of languages, with type disciplines in a spectrum between static and dynamic typing. Gradual session types address this mixed setting by providing a framework which grants seamless transition between statically typed handling of sessions and any required degree of dynamic typing. We propose Gradual GV as a gradually typed extension of the functional session type system GV. Following a standard framework of gradual typing, Gradual GV consists of an external language, which relaxes the type system of GV using dynamic types, and an internal language with casts, for which operational semantics is given, and a cast-insertion translation from the former to the latter. We demonstrate type and communication safety as well as blame safety, thus extending previous results to functional languages with session-based communication. The interplay of linearity and dynamic types requires a novel approach to specifying the dynamics of the language. △ Less

Submitted 16 September, 2019; v1 submitted 15 September, 2018; originally announced September 2018.

Comments: Preprint of an article to appear in Journal of Functional Programming

Journal ref: J. Funct. Prog. 29 (2019) e17

LTL Semantic Tableaux and Alternating $ω$-automata via Linear Factors

Authors: Martin Sulzmann, Peter Thiemann

Abstract: Linear Temporal Logic (LTL) is a widely used specification framework for linear time properties of systems. The standard approach for verifying such properties is by transforming LTL formulae to suitable $ω$-automata and then applying model checking. We revisit Vardi's transformation of an LTL formula to an alternating $ω$-automaton and Wolper's LTL tableau method for satisfiability checking. We… ▽ More Linear Temporal Logic (LTL) is a widely used specification framework for linear time properties of systems. The standard approach for verifying such properties is by transforming LTL formulae to suitable $ω$-automata and then applying model checking. We revisit Vardi's transformation of an LTL formula to an alternating $ω$-automaton and Wolper's LTL tableau method for satisfiability checking. We observe that both constructions effectively rely on a decomposition of formulae into linear factors. Linear factors have been introduced previously by Antimirov in the context of regular expressions. We establish the notion of linear factors for LTL and verify essential properties such as expansion and finiteness. Our results shed new insights on the connection between the construction of alternating $ω$-automata and semantic tableaux. △ Less

Submitted 18 October, 2017; originally announced October 2017.

A Computational Interpretation of Context-Free Expressions

Authors: Martin Sulzmann, Peter Thiemann

Abstract: We phrase parsing with context-free expressions as a type inhabitation problem where values are parse trees and types are context-free expressions. We first show how containment among context-free and regular expressions can be reduced to a reachability problem by using a canonical representation of states. The proofs-as-programs principle yields a computational interpretation of the reachability… ▽ More We phrase parsing with context-free expressions as a type inhabitation problem where values are parse trees and types are context-free expressions. We first show how containment among context-free and regular expressions can be reduced to a reachability problem by using a canonical representation of states. The proofs-as-programs principle yields a computational interpretation of the reachability problem in terms of a coercion that transforms the parse tree for a context-free expression into a parse tree for a regular expression. It also yields a partial coercion from regular parse trees to context-free ones. The partial coercion from the trivial language of all words to a context-free expression corresponds to a predictive parser for the expression. △ Less

Submitted 24 August, 2017; originally announced August 2017.

Static Contract Simplification

Authors: Matthias Keil, Peter Thiemann

Abstract: Contracts and contract monitoring are a powerful mechanism for specifying properties and guaranteeing them at run time. However, run time monitoring of contracts imposes a significant overhead. The execution time is impacted by the insertion of contract checks as well as by the introduction of proxy objects that perform delayed contract checks on demand. Static contract simplification attacks th… ▽ More Contracts and contract monitoring are a powerful mechanism for specifying properties and guaranteeing them at run time. However, run time monitoring of contracts imposes a significant overhead. The execution time is impacted by the insertion of contract checks as well as by the introduction of proxy objects that perform delayed contract checks on demand. Static contract simplification attacks this issue using program transformation. It applies compile-time transformations to programs with contracts to reduce the overall run time while preserving the original behavior. Our key technique is to statically propagate contracts through the program and to evaluate and merge contracts where possible. The goal is to obtain residual contracts that are collectively cheaper to check at run time. We distinguish different levels of preservation of behavior, which impose different limitations on the admissible transformations: Strong blame preservation, where the transformation is a behavioral equivalence, and weak blame preservation, where the transformed program is equivalent up to the particular violation reported. Our transformations never increase the overall number of contract checks. △ Less

Submitted 30 March, 2017; originally announced March 2017.

Comments: Technical Report

Transaction-based Sandboxing for JavaScript

Authors: Matthias Keil, Peter Thiemann

Abstract: Today's JavaScript applications are composed of scripts from different origins that are loaded at run time. As not all of these origins are equally trusted, the execution of these scripts should be isolated from one another. However, some scripts must access the application state and some may be allowed to change it, while preserving the confidentiality and integrity constraints of the application… ▽ More Today's JavaScript applications are composed of scripts from different origins that are loaded at run time. As not all of these origins are equally trusted, the execution of these scripts should be isolated from one another. However, some scripts must access the application state and some may be allowed to change it, while preserving the confidentiality and integrity constraints of the application. This paper presents design and implementation of DecentJS, a language-embedded sandbox for full JavaScript. It enables scripts to run in a configurable degree of isolation with fine-grained access control. It provides a transactional scope in which effects are logged for review by the access control policy. After inspection of the log, effects can be committed to the application state or rolled back. The implementation relies on JavaScript proxies to guarantee full interposition for the full language and for all code, including dynamically loaded scripts and code injected via eval. Its only restriction is that scripts must be compliant with JavaScript's strict mode. △ Less

Submitted 17 January, 2017; v1 submitted 2 December, 2016; originally announced December 2016.

Comments: Technical Report

Partial Derivatives for Context-Free Languages: From $μ$-Regular Expressions to Pushdown Automata

Authors: Peter Thiemann

Abstract: We extend Antimirov's partial derivatives from regular expressions to $μ$-regular expressions that describe context-free languages. We prove the correctness of partial derivatives as well as the finiteness of the set of iterated partial derivatives. The latter are used as pushdown symbols in our construction of a nondeterministic pushdown automaton, which generalizes Antimirov's NFA construction. We extend Antimirov's partial derivatives from regular expressions to $μ$-regular expressions that describe context-free languages. We prove the correctness of partial derivatives as well as the finiteness of the set of iterated partial derivatives. The latter are used as pushdown symbols in our construction of a nondeterministic pushdown automaton, which generalizes Antimirov's NFA construction. △ Less

Submitted 2 January, 2017; v1 submitted 21 October, 2016; originally announced October 2016.

Comments: 22 pages = 15 pages + bibliography + proofs; accepted by FoSSaCS 2017

MSC Class: 68Q45

Static Trace-Based Deadlock Analysis for Synchronous Mini-Go

Authors: Kai Stadtmüller, Martin Sulzmann, Peter Thiemann

Abstract: We consider the problem of static deadlock detection for programs in the Go programming language which make use of synchronous channel communications. In our analysis, regular expressions extended with a fork operator capture the communication behavior of a program. Starting from a simple criterion that characterizes traces of deadlock-free programs, we develop automata-based methods to check for… ▽ More We consider the problem of static deadlock detection for programs in the Go programming language which make use of synchronous channel communications. In our analysis, regular expressions extended with a fork operator capture the communication behavior of a program. Starting from a simple criterion that characterizes traces of deadlock-free programs, we develop automata-based methods to check for deadlock-freedom. The approach is implemented and evaluated with a series of examples. △ Less

Submitted 2 September, 2016; v1 submitted 30 August, 2016; originally announced August 2016.

Derivatives for Enhanced Regular Expressions

Authors: Peter Thiemann

Abstract: Regular languages are closed under a wealth of formal language operators. Incorporating such operators in regular expressions leads to concise language specifications, but the transformation of such enhanced regular expressions to finite automata becomes more involved. We present an approach that enables the direct construction of finite automata from regular expressions enhanced with further op… ▽ More Regular languages are closed under a wealth of formal language operators. Incorporating such operators in regular expressions leads to concise language specifications, but the transformation of such enhanced regular expressions to finite automata becomes more involved. We present an approach that enables the direct construction of finite automata from regular expressions enhanced with further operators that preserve regularity. Our construction is based on an extension of the theory of derivatives for regular expressions. To retain the standard results about derivatives, we develop a derivability criterion for the compatibility of the extra operators with derivatives. Some derivable operators do not preserve regularity. Derivatives provide a decision procedure for the word problem of regular expressions enhanced with such operators. △ Less

Submitted 3 May, 2016; originally announced May 2016.

Comments: To appear in CIAA 2016

MSC Class: 68Q45

Forkable Regular Expressions

Authors: Martin Sulzmann, Peter Thiemann

Abstract: We consider forkable regular expressions, which enrich regular expressions with a fork operator, to establish a formal basis for static and dynamic analysis of the communication behavior of concurrent programs. We define a novel compositional semantics for forkable expressions, establish their fundamental properties, and define derivatives for them as a basis for the generation of automata, for ma… ▽ More We consider forkable regular expressions, which enrich regular expressions with a fork operator, to establish a formal basis for static and dynamic analysis of the communication behavior of concurrent programs. We define a novel compositional semantics for forkable expressions, establish their fundamental properties, and define derivatives for them as a basis for the generation of automata, for matching, and for language containment tests. Forkable expressions may give rise to non-regular languages, in general, but we identify sufficient conditions on expressions that guarantee finiteness of the automata construction via derivatives. △ Less

Submitted 8 December, 2015; v1 submitted 25 October, 2015; originally announced October 2015.

Comments: 12 pages plus technical appendix, to appear in LATA 2016

Combining behavioural types with security analysis

Authors: Massimo Bartoletti, Ilaria Castellani, Pierre-Malo Deniélou, Mariangiola Dezani-Ciancaglini, Silvia Ghilezan, Jovanka Pantovic, Jorge A. Pérez, Peter Thiemann, Bernardo Toninho, Hugo Torres Vieira

Abstract: Today's software systems are highly distributed and interconnected, and they increasingly rely on communication to achieve their goals; due to their societal importance, security and trustworthiness are crucial aspects for the correctness of these systems. Behavioural types, which extend data types by describing also the structured behaviour of programs, are a widely studied approach to the enforc… ▽ More Today's software systems are highly distributed and interconnected, and they increasingly rely on communication to achieve their goals; due to their societal importance, security and trustworthiness are crucial aspects for the correctness of these systems. Behavioural types, which extend data types by describing also the structured behaviour of programs, are a widely studied approach to the enforcement of correctness properties in communicating systems. This paper offers a unified overview of proposals based on behavioural types which are aimed at the analysis of security properties. △ Less

Submitted 8 October, 2015; originally announced October 2015.

Journal ref: Journal of Logical and Algebraic Methods in Programming, Elsevier, 2015, pp.18

TreatJS: Higher-Order Contracts for JavaScript

Authors: Matthias Keil, Peter Thiemann

Abstract: TreatJS is a language embedded, higher-order contract system for JavaScript which enforces contracts by run-time monitoring. Beyond providing the standard abstractions for building higher-order contracts (base, function, and object contracts), TreatJS's novel contributions are its guarantee of non-interfering contract execution, its systematic approach to blame assignment, its support for contract… ▽ More TreatJS is a language embedded, higher-order contract system for JavaScript which enforces contracts by run-time monitoring. Beyond providing the standard abstractions for building higher-order contracts (base, function, and object contracts), TreatJS's novel contributions are its guarantee of non-interfering contract execution, its systematic approach to blame assignment, its support for contracts in the style of union and intersection types, and its notion of a parameterized contract scope, which is the building block for composable run-time generated contracts that generalize dependent function contracts. TreatJS is implemented as a library so that all aspects of a contract can be specified using the full JavaScript language. The library relies on JavaScript proxies to guarantee full interposition for contracts. It further exploits JavaScript's reflective features to run contracts in a sandbox environment, which guarantees that the execution of contract code does not modify the application state. No source code transformation or change in the JavaScript run-time system is required. The impact of contracts on execution speed is evaluated using the Google Octane benchmark. △ Less

Submitted 30 April, 2015; originally announced April 2015.

Comments: Technical Report

ACM Class: D.2.4

Transparent Object Proxies for JavaScript

Authors: Matthias Keil, Sankha Narayan Guria, Andreas Schlegel, Manuel Geffken, Peter Thiemann

Abstract: Proxies are the swiss army knives of object adaptation. They introduce a level of indirection to intercept select operations on a target object and divert them as method calls to a handler. Proxies have many uses like implementing access control, enforcing contracts, virtualizing resources. One important question in the design of a proxy API is whether a proxy object should inherit the identity… ▽ More Proxies are the swiss army knives of object adaptation. They introduce a level of indirection to intercept select operations on a target object and divert them as method calls to a handler. Proxies have many uses like implementing access control, enforcing contracts, virtualizing resources. One important question in the design of a proxy API is whether a proxy object should inherit the identity of its target. Apparently proxies should have their own identity for security-related applications whereas other applications, in particular contract systems, require transparent proxies that compare equal to their target objects. We examine the issue with transparency in various use cases for proxies, discuss different approaches to obtain transparency, and propose two designs that require modest modifications in the JavaScript engine and cannot be bypassed by the programmer. We implement our designs in the SpiderMonkey JavaScript interpreter and bytecode compiler. Our evaluation shows that these modifications of have no statistically significant impact on the benchmark performance of the JavaScript engine. Furthermore, we demonstrate that contract systems based on wrappers require transparent proxies to avoid interference with program execution in realistic settings. △ Less

Submitted 30 April, 2015; originally announced April 2015.

Comments: Technical Report

ACM Class: D.3.3

A Falsification View of Success Typing

Authors: Robert Jakob, Peter Thiemann

Abstract: Dynamic languages are praised for their flexibility and expressiveness, but static analysis often yields many false positives and verification is cumbersome for lack of structure. Hence, unit testing is the prevalent incomplete method for validating programs in such languages. Falsification is an alternative approach that uncovers definite errors in programs. A falsifier computes a set of inputs… ▽ More Dynamic languages are praised for their flexibility and expressiveness, but static analysis often yields many false positives and verification is cumbersome for lack of structure. Hence, unit testing is the prevalent incomplete method for validating programs in such languages. Falsification is an alternative approach that uncovers definite errors in programs. A falsifier computes a set of inputs that definitely crash a program. Success typing is a type-based approach to document programs in dynamic languages. We demonstrate that success typing is, in fact, an instance of falsification by mapping success (input) types into suitable logic formulae. Output types are represented by recursive types. We prove the correctness of our mapping (which establishes that success typing is falsification) and we report some experiences with a prototype implementation. △ Less

Submitted 5 February, 2015; v1 submitted 4 February, 2015; originally announced February 2015.

Comments: extended version

Symbolic Solving of Extended Regular Expression Inequalities

Authors: Matthias Keil, Peter Thiemann

Abstract: This paper presents a new solution to the containment problem for extended regular expressions that extends basic regular expressions with intersection and complement operators and consider regular expressions on infinite alphabets based on potentially infinite character sets. Standard approaches deciding the containment do not take extended operators or character sets into account. The algorithm… ▽ More This paper presents a new solution to the containment problem for extended regular expressions that extends basic regular expressions with intersection and complement operators and consider regular expressions on infinite alphabets based on potentially infinite character sets. Standard approaches deciding the containment do not take extended operators or character sets into account. The algorithm avoids the translation to an expression-equivalent automaton and provides a purely symbolic term rewriting systems for solving regular expressions inequalities. We give a new symbolic decision procedure for the containment problem based on Brzozowski's regular expression derivatives and Antimirov's rewriting approach to check containment. We generalize Brzozowski's syntactic derivative operator to two derivative operators that work with respect to (potentially infinite) representable character sets. △ Less

Submitted 13 October, 2014; originally announced October 2014.

Comments: Technical Report

On the Proxy Identity Crisis

Authors: Matthias Keil, Peter Thiemann

Abstract: A proxy, in general, is an object mediating access to an arbitrary target object. The proxy is then intended to be used in place of the target object. Ideally, a proxy is not distinguishable from other objects. Running a program with a proxy leads to the same outcome as running the program with the target object. Even though the approach provides a lot of power to the user, proxies come with a lim… ▽ More A proxy, in general, is an object mediating access to an arbitrary target object. The proxy is then intended to be used in place of the target object. Ideally, a proxy is not distinguishable from other objects. Running a program with a proxy leads to the same outcome as running the program with the target object. Even though the approach provides a lot of power to the user, proxies come with a limitation. Because a proxy, wrapping a target object, is a new object and different from its target, the interposition changes the behaviour of some core components. For distinct proxies the double == and triple === equal operator returns false, even if the target object is the same. More precisely, the expected result depends on use case. To overcome this limitation we will discuss alternatives. △ Less

Submitted 19 December, 2013; originally announced December 2013.

Comments: Position Paper

Efficient Dynamic Access Analysis Using JavaScript Proxies

Authors: Matthias Keil, Peter Thiemann

Abstract: JSConTest introduced the notions of effect monitoring and dynamic effect inference for JavaScript. It enables the description of effects with path specifications resembling regular expressions. It is implemented by an offline source code transformation. To overcome the limitations of the JSConTest implementation, we redesigned and reimplemented effect monitoring by taking advantange of JavaScrip… ▽ More JSConTest introduced the notions of effect monitoring and dynamic effect inference for JavaScript. It enables the description of effects with path specifications resembling regular expressions. It is implemented by an offline source code transformation. To overcome the limitations of the JSConTest implementation, we redesigned and reimplemented effect monitoring by taking advantange of JavaScript proxies. Our new design avoids all drawbacks of the prior implementation. It guarantees full interposition; it is not restricted to a subset of JavaScript; it is self-maintaining; and its scalability to large programs is significantly better than with JSConTest. The improved scalability has two sources. First, the reimplementation is significantly faster than the original, transformation-based implementation. Second, the reimplementation relies on the fly-weight pattern and on trace reduction to conserve memory. Only the combination of these techniques enables monitoring and inference for large programs. △ Less

Submitted 11 December, 2013; originally announced December 2013.

Comments: Technical Report

Towards Tree Automata-based Success Types

Authors: Robert Jakob, Peter Thiemann

Abstract: Error detection facilities for dynamic languages are often based on unit testing. Thus, the advantage of rapid prototyping and flexibility must be weighed against cumbersome and time consuming test suite development. Lindahl and Sagonas' success typings provide a means of static must-fail detection in Erlang. Due to the constraint-based nature of the approach, some errors involving nested tuples a… ▽ More Error detection facilities for dynamic languages are often based on unit testing. Thus, the advantage of rapid prototyping and flexibility must be weighed against cumbersome and time consuming test suite development. Lindahl and Sagonas' success typings provide a means of static must-fail detection in Erlang. Due to the constraint-based nature of the approach, some errors involving nested tuples and recursion cannot be detected. We propose an approach that uses an extension of model checking for pattern-matching recursion schemes with context-aware ranked tree automata to provide improved success typings for a constructor-based first-order prototype language. △ Less

Submitted 21 June, 2013; originally announced June 2013.

Comments: Abstract presented at HOPA 2013

Type-based Dependency Analysis for JavaScript

Authors: Matthias Keil, Peter Thiemann

Abstract: Dependency analysis is a program analysis that determines potential data flow between program points. While it is not a security analysis per se, it is a viable basis for investigating data integrity, for ensuring confidentiality, and for guaranteeing sanitization. A noninterference property can be stated and proved for the dependency analysis. We have designed and implemented a dependency analysi… ▽ More Dependency analysis is a program analysis that determines potential data flow between program points. While it is not a security analysis per se, it is a viable basis for investigating data integrity, for ensuring confidentiality, and for guaranteeing sanitization. A noninterference property can be stated and proved for the dependency analysis. We have designed and implemented a dependency analysis for JavaScript. We formalize this analysis as an abstraction of a tainting semantics. We prove the correctness of the tainting semantics, the soundness of the abstraction, a noninterference property, and the termination of the analysis. △ Less

Submitted 29 May, 2013; originally announced May 2013.

Comments: Technical Report