SearcharxivSearch

arXiv subjects

Zachary Kent

Publications and source records attributed to Zachary Kent.

3 recordsLinked to original sources

uSTM: A Lightweight and Efficient STM Supporting General Types and Deferred Aborts

Software Transactional Memory (STM) systems allow developers to more easily exploit multicore architectures by wrapping arbitrary sequential code in transactions that are executed concurrently. In recent years, the performance of STM systems has approached that of hand-tuned data structures through techniques that avoid unnecessary aborts and exploit the semantics of underlying data structures. Despite achieving excellent performance, most STM systems do not fully address the concerns they targeted in the first place: safety, usability, and generality. In particular, these systems place restrictions on the data types that may be updated transactionally, such as requiring that these types fit within a word, and can require modification of data layout. Moreover, most STM systems abort transactions in the middle of client code to ensure correctness. This can cause space leaks and other bugs not present in the original code. We present ustm, a novel STM system addressing all of these shortcomings while still maintaining excellent performance, all within ~300 lines of code. uSTM supports general types while maintaining data layout. Aborts are deferred until the end of the transaction, allowing client code within a transaction to terminate normally. To ensure that uSTM guarantees opacity, we implement a novel timestamping algorithm we call split-increment timestamps. We compare the performance of uSTM to a variety of state-of-the-art (SOTA) STM systems, demonstrating that uSTM matches or outperforms the SOTA on a variety of workloads.

cs.DC

Mechanized Metatheory of Forward Reasoning for End-to-End Linearizability Proofs

In the past decade, many techniques have been developed to prove linearizability, the gold standard of correctness for concurrent data structures. Intuitively, linearizability requires that every operation on a concurrent data structure appears to take place instantaneously, even when interleaved with other operations. Most recently, Jayanti et al. presented the first sound and complete "forward reasoning" technique for proving linearizability that relates the behavior of a concurrent data structure to a reference atomic data structure as time moves forward. This technique can be used to produce machine-checked proofs of linearizability in TLA+. However, while Jayanti et al.'s approach is shown to be sound and complete, a mechanization of this important metatheoretic result is still outstanding. As a result, it is not possible to produce verified end-to-end proofs of linearizability. To reduce the size of this trusted computing base, we formalize this forward reasoning technique and mechanize proofs of its soundness and completeness in Rocq. As a case study, we use the approach to produce a verified end-to-end proof of linearizability for a simple concurrent register.

cs.PL

Congruences for Taylor expansions of quantum modular forms

Recently, a beautiful paper of Andrews and Sellers has established linear congruences for the Fishburn numbers modulo an infinite set of primes. Since then, a number of authors have proven refined results, for example, extending all of these congruences to arbitrary powers of the primes involved. Here, we take a different perspective and explain the general theory of such congruences in the context of an important class of quantum modular forms. As one example, we obtain an infinite series of combinatorial sequences connected to the "half-derivatives" of the Andrews-Gordon functions and with Kashaev's invariant on $(2m+1,2)$ torus knots, and we prove conditions under which the sequences satisfy linear congruences modulo at least $50\%$ of primes of primes.

math.NT