arXiv subjects

Martin Sulzmann

Publications and source records attributed to Martin Sulzmann.

At least 19 recordsLinked to original sources

arXiv2026

Critical Sections Are Not Per-Thread: A Trace Semantics for Lock-Based Concurrency

Locks are a standard mechanism for synchronizing concurrent threads. The standard lock set construction assumes that critical sections are confined to a single thread, and therefore only accounts for locks acquired within that thread. Traditional definitions of critical sections implicitly assume that protected events belong to the same thread. We demonstrate that this assumption does not hold for general C/Pthread executions. Using a trace model that captures the essence of C/Pthread programs, we give a trace-based characterization of critical sections that does not impose a per-thread restriction. As a result, critical sections may span multiple threads. Such \emph{multi-thread} critical sections arise naturally in real programs and close a semantic gap in the standard lock set construction.

cs.PL↗

arXiv2025

Beyond Per-Thread Lock Sets: Multi-Thread Critical Sections and Dynamic Deadlock Prediction

Lock sets are commonly used for dynamic analysis of deadlocks. The standard per-thread lock set construction only considers locks acquired in the same thread, but is unaware of locks acquired in another thread. This leads to false positives and false negatives. The underlying issue is that the commonly used notion of a critical section on which the lock set construction relies ignores events from other threads. We give a trace-based characterization of critical sections that drops this restriction. Critical sections are no longer restricted to a single thread and can cover multiple threads. Such forms of critical sections exist, are natural, and correct the standard formulation. We show how to soundly approximate the trace-based characterization via partial order relations. Thus, we obtain an improved lock set construction that can still be efficiently computed and allows us to remove false positives reported by the DIRK deadlock predictor and remove false negatives by extending the SPDOffline deadlock predictor. We integrate various lock set constructions with increased precision in an extension of SPDOffline. Our extensions remain sound (no false positives) but are more complete (fewer false negatives) w.r.t. SPDOffline. For an extensive standard benchmark suite we can also show that the performance is not affected.

cs.PL↗

arXiv2025

Partial Orders for Precise and Efficient Dynamic Deadlock Prediction

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.

cs.PL↗

arXiv2023

Cross-thread critical sections and efficient dynamic race prediction methods

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.

cs.PL↗

arXiv2022

A Type-Directed, Dictionary-Passing Translation of Method Overloading and Structural Subtyping in Featherweight Generic Go

Featherweight Generic Go (FGG) is a minimal core calculus modeling the essential features of the programming language Go. It includes support for overloaded methods, interface types, structural subtyping and generics. The most straightforward semantic description of the dynamic behavior of FGG programs is to resolve method calls based on runtime type information of the receiver. This article shows a different approach by defining a type-directed translation from FGG- to an untyped lambda-calculus. FGG- includes all features of FGG but type assertions. The translation of an FGG- program provides evidence for the availability of methods as additional dictionary parameters, similar to the dictionary-passing approach known from Haskell type classes. Then, method calls can be resolved by a simple lookup of the method definition in the dictionary. Every program in the image of the translation has the same dynamic semantics as its source FGG- program. The proof of this result is based on a syntactic, step-indexed logical relation. The step-index ensures a well-founded definition of the relation in the presence of recursive interface types and recursive methods. Although being non-deterministic, the translation is coherent.

cs.PL↗

arXiv2022

Semantic preservation for a type directed translation scheme of Featherweight Go

Featherweight Go (FG) is a minimal core calculus that includes essential Go features such as overloaded methods and interface types. The most straightforward semantic description of the dynamic behavior of FG programs is to resolve method calls based on run-time type information. A more efficient approach is to apply a type-directed translation scheme where interface-values are replaced by dictionaries that contain concrete method definitions. Thus, method calls can be resolved by a simple lookup of the method definition in the dictionary. Establishing that the target program obtained via the type-directed translation scheme preserves the semantics of the original FG program is an important task. To establish this property we employ logical relations that are indexed by types to relate source and target programs. We provide rigorous proofs and give a detailed discussion of the many subtle corners that we have encountered including the need for a step index due to recursive interfaces and method definitions.

cs.PL↗

arXiv2021

A Dictionary-Passing Translation of Featherweight Go

The Go programming language is an increasingly popular language but some of its features lack a formal investigation. This article explains Go's resolution mechanism for overloaded methods and its support for structural subtyping by means of translation from Featherweight Go to a simple target language. The translation employs a form of dictionary passing known from type classes in Haskell and preserves the dynamic behavior of Featherweight Go programs.

cs.PL↗

arXiv2020

Visual Testing of GUIs by Abstraction

Ensuring the correct visual appearance of graphical user interfaces (GUIs) is important because visual bugs can cause substantial losses for businesses. An application might behave functionally correct in an automated test, but visual bugs can make the GUI effectively unusable for the user. Most of today's approaches for visual testing are pixel-based and tend to have flaws that are characteristic for image differencing. For instance, minor and unimportant visual changes often cause false positives, which confuse the user with unnecessary error reports. Our idea is to introduce an abstract GUI state (AGS), where we define structural relations to identify relevant GUI changes and ignore those that are unimportant from the user's point of view. In addition, we explore several strategies to address the GUI element identification problem in terms of AGS. This allows us to provide rich diagnostic information that help the user to better interpret changes. Based on the principles of golden master testing, we can support a fully-automated approach to visual testing by using the AGS. We have implemented our approach to visually test web pages and our experiments show that we are able to reliably detect GUI changes.

cs.SE↗

arXiv2020

Efficient, Near Complete and Often Sound Hybrid Dynamic Data Race Prediction (extended version)

Dynamic data race prediction aims to identify races based on a single program run represented by a trace. The challenge is to remain efficient while being as sound and as complete as possible. Efficient means a linear run-time as otherwise the method unlikely scales for real-world programs. We introduce an efficient, near complete and often sound dynamic data race prediction method that combines the lockset method with several improvements made in the area of happens-before methods. By near complete we mean that the method is complete in theory but for efficiency reasons the implementation applies some optimizations that may result in incompleteness. The method can be shown to be sound for two threads but is unsound in general. We provide extensive experimental data that shows that our method works well in practice.

cs.PL↗

arXiv2019

Predicting All Data Race Pairs for a Specific Schedule (extended version)

We consider the problem of data race prediction where the program's behavior is represented by a trace. A trace is a sequence of program events recorded during the execution of the program. We employ the schedulable happens-before relation to characterize all pairs of events that are in a race for the schedule as manifested in the trace. Compared to the classic happens-before relation, the schedulable happens-before relations properly takes care of write-read dependencies and thus avoids false positives. The challenge is to efficiently identify all (schedulable) data race pairs. We present a refined linear time vector clock algorithm to predict many of the schedulable data race pairs. We introduce a quadratic time post-processing algorithm to predict all remaining data race pairs. This improves the state of the art in the area and our experiments show that our approach scales to real-world examples. Thus, the user can systematically examine and fix all program locations that are in a race for a particular schedule.

cs.PL↗

arXiv2019

Solving of Regular Equations Revisited (extended version)

Solving of regular equations via Arden's Lemma is folklore knowledge. We first give a concise algorithmic specification of all elementary solving steps. We then discuss a computational interpretation of solving in terms of coercions that transform parse trees of regular equations into parse trees of solutions. Thus, we can identify some conditions on the shape of regular equations under which resulting solutions are unambiguous. We apply our result to convert a DFA to an unambiguous regular expression. In addition, we show that operations such as subtraction and shuffling can be expressed via some appropriate set of regular equations. Thus, we obtain direct (algebraic) methods without having to convert to and from finite automaton.

cs.FL↗

arXiv2019

Data Race Prediction for Inaccurate Traces

Happens-before based data race prediction methods infer from a trace of events a partial order to check if one event happens before another event. If two two write events are unordered, they are in a race. We observe that common tracing methods provide no guarantee that the trace order corresponds to an actual program run. The consequence of inaccurate tracing is that results (races) reported are inaccurate. We introduce diagnostic methods to examine if (1) a race is guaranteed to be correct regardless of any potential inaccuracies, (2) maybe is incorrect due to inaccurate tracing. We have fully implemented the approach and provide for an empirical comparison with state of the art happens-before based race predictors such as FastTrack and SHB.

cs.PL↗

arXiv2018

Two-Phase Dynamic Analysis of Message-Passing Go Programs based on Vector Clocks

Understanding the run-time behavior of concurrent programs is a challenging task. A popular approach is to establish a happens- before relation via vector clocks. Thus, we can identify bugs and per- formance bottlenecks, for example, by checking if two con icting events may happen concurrently. We employ a two-phase method to derive vector clock information for a wide range of concurrency features that includes all of the message-passing features in Go. The rst phase (instrumentation and tracing) yields a run-time trace that records all events related to message-passing concurrency that took place. The second phase (trace replay) is carried out o ine and replays the recorded traces to infer vector clock information. Trace replay operates on thread-local traces. Thus, we can observe behav- ior that might result from some alternative schedule. Our approach is not tied to any speci c language. We have built a prototype for the Go programming language and provide empirical evidence of the usefulness of our method.

cs.PL↗

arXiv2017

LTL Semantic Tableaux and Alternating $\omega$-automata via Linear Factors

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 $\omega$-automata and then applying model checking. We revisit Vardi's transformation of an LTL formula to an alternating $\omega$-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 $\omega$-automata and semantic tableaux.

cs.FL↗

arXiv2017

Trace-Based Run-time Analysis of Message-Passing Go Programs

We consider the task of analyzing message-passing programs by observing their run-time behavior. We introduce a purely library-based instrumentation method to trace communication events during execution. A model of the dependencies among events can be constructed to identify potential bugs. Compared to the vector clock method, our approach is much simpler and has in general a significant lower run-time overhead. A further advantage is that we also trace events that could not commit. Thus, we can infer alternative communications. This provides the user with additional information to identify potential bugs. We have fully implemented our approach in the Go programming language and provide a number of examples to substantiate our claims.

cs.PL↗

arXiv2017

A Computational Interpretation of Context-Free Expressions

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.

cs.FL↗

arXiv2016

Static Trace-Based Deadlock Analysis for Synchronous Mini-Go

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.

cs.PL↗

arXiv2016

Derivative-Based Diagnosis of Regular Expression Ambiguity

Regular expressions are often ambiguous. We present a novel method based on Brzozowski's derivatives to aid the user in diagnosing ambiguous regular expressions. We introduce a derivative-based finite state transducer to generate parse trees and minimal counter-examples. The transducer can be easily customized to either follow the POSIX or Greedy disambiguation policy and based on a finite set of examples it is possible to examine if there are any differences among POSIX and Greedy.

cs.FL↗