arXiv subjects

Tobias Wrigstad

Publications and source records attributed to Tobias Wrigstad.

14 recordsLinked to original sources

arXiv2026

Floating-Point Usage on GitHub: A Large-Scale Study of Statically Typed Languages

Reasoning about floating-point arithmetic is notoriously hard. While static and dynamic analysis techniques or program repair have made significant progress, more work is still needed to make them relevant to real-world code. On the critical path to that goal is understanding what real-world floating-point code looks like. To close that knowledge gap, this paper presents the first large-scale empirical study of floating-point arithmetic usage across public GitHub repositories. We focus on statically typed languages to allow our study to scale to millions of repositories. We follow state-of the art mining practices including random sampling and filtering based on only intrinsic properties to avoid bias, and identify floating-point usage by searching for keywords in the source code, and programming language constructs (e.g., loops) by parsing the code. Our evaluation supports the claim often made in papers that floating-point arithmetic is widely used. Comparing statistics such as size and usage of certain constructs and functions, we find that benchmarks used in literature to evaluate automated reasoning techniques for floating-point arithmetic are in certain aspects representative of 'real-world' code, but not in all. We publish a dataset of 10 million real-world floating-point functions extracted from our study. We demonstrate in a case study how it may be used to identify new floating-point benchmarks and help future techniques for floating-point arithmetic to be designed and evaluated to match actual users' expectations.

cs.PL↗

arXiv2025

Monk: Opportunistic Scheduling to Delay Horizontal Scaling

In modern server computing, efficient CPU resource usage is often traded for latency. Garbage collection is a key aspect of memory management in programming languages like Java, but it often competes with application threads for CPU time, leading to delays in processing requests and consequent increases in latency. This work explores if opportunistic scheduling in ZGC, a fully concurrent garbage collector (GC), can reduce application latency on middle-range CPU utilization, a topical deployment, and potentially delay horizontal scaling. We implemented an opportunistic scheduling that schedules GC threads during periods when CPU resources would otherwise be idle. This method prioritizes application threads over GC workers when it matters most, allowing the system to handle higher workloads without increasing latency. Our findings show that this technique can significantly improve performance in server applications. For example, in tests using the SPECjbb2015 benchmark, we observed up to a 15\% increase in the number of requests processed within the target 25ms latency. Additionally, applications like Hazelcast showed a mean latency reduction of up to 40% compared to ZGC without opportunistic scheduling. The feasibility and effectiveness of this approach were validated through empirical testing on two widely used benchmarks, showing that the method consistently improves performance under various workloads. This work is significant because it addresses a common bottleneck in server performance -- how to manage GC without degrading application responsiveness. By improving how GC threads are scheduled, this research offers a pathway to more efficient resource usage, enabling higher performance and better scalability in server applications.

cs.PL↗

arXiv2024

Scheduling Garbage Collection for Energy Efficiency on Asymmetric Multicore Processors

The growing concern for energy efficiency in the Information and Communication Technology (ICT) sector has prompted the exploration of resource management techniques. While hardware architectures, such as single-ISA asymmetric multicore processors (AMP), offer potential energy savings, there is still untapped potential for software optimizations. This paper aims to bridge this gap by investigating the scheduling of garbage collection (GC) activities on a heterogeneous architecture with both performance cores ("p-cores") and energy cores ("e-cores") to achieve energy savings. Our study focuses on the concurrent ZGC collector in the context of Java Virtual Machines (JVM), as the energy aspect is not well studied in the context of latency-sensitive Java workloads. By comparing the energy efficiency, performance, latency, and memory utilization of executing GC on p-cores versus e-cores, we present compelling findings. We demonstrate that scheduling GC work on e-cores overall leads to approximately 3% energy savings without performance and mean latency degradation while requiring no additional effort from developers. Overall energy reduction can increase to 5.3$\pm$0.0225% by tuning the number of e-cores (still not changing the program!). Our findings highlight the practicality and benefits of scheduling GC on e-cores, showcasing the potential for energy savings in heterogeneous architectures running Java workloads while meeting critical latency requirements. Our research contributes to the ongoing efforts toward achieving a more sustainable and efficient ICT sector.

cs.PL↗

arXiv2023

Reference Capabilities for Flexible Memory Management: Extended Version

Verona is a concurrent object-oriented programming language that organises all the objects in a program into a forest of isolated regions. Memory is managed locally for each region, so programmers can control a program's memory use by adjusting objects' partition into regions, and by setting each region's memory management strategy. A thread can only mutate (allocate, deallocate) objects within one active region -- its "window of mutability". Memory management costs are localised to the active region, ensuring overheads can be predicted and controlled. Moving the mutability window between regions is explicit, so code can be executed wherever it is required, yet programs remain in control of memory use. An ownership type system based on reference capabilities enforces region isolation, controlling aliasing within and between regions, yet supporting objects moving between regions and threads. Data accesses never need expensive atomic operations, and are always thread-safe.

cs.PL↗

arXiv2022

Rusty Links in Local Chains

Rust successfully applies ownership types to control memory allocation. This restricts the programs' topologies to the point where doubly-linked lists cannot be programmed in Safe Rust. We sketch how more flexible "local" ownership could be added to Rust, permitting multiple mutable references to objects, provided each reference is bounded by the object's lifetime. To maintain thread-safety, locally owned objects must remain thread-local; to maintain memory safety, local objects can be deallocated when their owner's lifetime expires.

cs.PL↗

arXiv2021

Dala: A Simple Capability-Based Dynamic Language Design For Data Race-Freedom

Dynamic languages like Erlang, Clojure, JavaScript, and E adopted data-race freedom by design. To enforce data-race freedom, these languages either deep copy objects during actor (thread) communication or proxy back to their owning thread. We present Dala, a simple programming model that ensures data-race freedom while supporting efficient inter-thread communication. Dala is a dynamic, concurrent, capability-based language that relies on three core capabilities: immutable values can be shared freely; isolated mutable objects can be transferred between threads but not aliased; local objects can be aliased within their owning thread but not dereferenced by other threads. Objects with capabilities can co-exist with unsafe objects, that are unchecked and may suffer data races, without compromising the safety of safe objects. We present a formal model of Dala, prove data race-freedom and state and prove a dynamic gradual guarantee. These theorems guarantee data race-freedom when using safe capabilities and show that the addition of capabilities is semantics preserving modulo permission and cast errors.

cs.PL↗

arXiv2021

Jupyter Notebooks on GitHub: Characteristics and Code Clones

Jupyter notebooks has emerged as a standard tool for data science programming. Programs in Jupyter notebooks are different from typical programs as they are constructed by a collection of code snippets interleaved with text and visualisation. This allows interactive exploration and snippets may be executed in different order which may give rise to different results due to side-effects between snippets. Previous studies have shown the presence of considerable code duplication -- code clones -- in sources of traditional programs, in both so-called systems programming languages and so-called scripting languages. In this paper we present the first large-scale study of code cloning in Jupyter notebooks. We analyse a corpus of 2.7 million Jupyter notebooks hosted on GitHJub, representing 37 million individual snippets and 227 million lines of code. We study clones at the level of individual snippets, and study the extent to which snippets are recurring across multiple notebooks. We study both identical clones and approximate clones and conduct a small-scale ocular inspection of the most common clones. We find that code cloning is common in Jupyter notebooks -- more than 70% of all code snippets are exact copies of other snippets (with possible differences in white spaces), and around 50% of all notebooks do not have any unique snippet, but consists solely of snippets that are also found elsewhere. In notebooks written in Python, at least 80% of all snippets are approximate clones and the prevalence of code cloning is higher in Python than in other languages. We further find that clones between different repositories are far more common than clones within the same repository. However, the most common individual repository from which a Jupyter notebook contains clones is the repository in which itself resides.

cs.SE↗

arXiv2019

Towards Gradual Checking of Reference Capabilities

Concurrent and parallel programming is difficult due to the presence of memory side-effects, which may introduce data races. Type qualifiers, such as reference capabilities, can remove data races by restricting sharing of mutable data. Unfortunately, reference capability languages are an all-in or nothing game, i.e., all the types must be annotated with reference capabilities. In this work in progress, we propose to mix the ideas from the reference capability literature with gradual typing, leading to gradual reference capabilities.

cs.PL↗

arXiv2019

Reference Capabilities for Safe Parallel Array Programming

The array is a fundamental data structure that provides an efficient way to store and retrieve non-sparse data contiguous in memory. Arrays are important for the performance of many memory-intensive applications due to the design of modern memory hierarchies: contiguous storage facilitates spatial locality and predictive access patterns which enables prefetching. Operations on large arrays often lend themselves well to parallelisation, such as a fork-join style divide-and-conquer algorithm for sorting. For parallel operations on arrays to be deterministic, data-race freedom must be guaranteed. For operations on arrays of primitive data, data-race freedom is obtained by coordinating accesses so that no two threads operate on the same array indices. This is however not enough for arrays of non-primitives due to aliasing: accesses of separate array elements may return pointers to the same object, or overlapping structures. Reference capabilities have been used successfully in the past to statically guarantee the absence of data-races in object-oriented programs. This paper presents the first extension of reference capabilities -- called array capabilities -- that support concurrent and parallel operations on arrays of both primitive and non-primitive values. In addition to element access, array capabilities support the abstract manipulation of arrays, logical splitting of arrays into subarrays, and merging subarrays. These operations allow expressing a wide range of array use cases. This paper presents the array capability design space and show how it applies to a number of array use cases. The core ideas are formalised and proven sound in a simple calculus, along with a proof that shows that well-typed programs with array capabilities are free from data-races.

cs.PL↗

arXiv2019

Mastery Learning-Like Teaching with Achievements

This paper describes the design of a second-year, 20 ECTS credit course on imperative and object-oriented programming. The key design rhetoric is encouraging students to assume responsibility for their own learning, and, to this end, elements from mastery learning and other teaching strategies are used in concert to construct an achievement-based system where students are put in charge of how and when they are examined. In addition to describing the elements of the course design, the paper reports on experiences from teaching in this format, and how the format has evolved over time.

cs.CY↗

arXiv2019

Safely Abstracting Memory Layouts

Modern architectures require applications to make effective use of caches to achieve high performance and hide memory latency. This in turn requires careful consideration of placement of data in memory to exploit spatial locality, leverage hardware prefetching and conserve memory bandwidth. In unmanaged languages like C++, memory optimisations are common, but at the cost of losing object abstraction and memory safety. In managed languages like Java and C#, the abstract view of memory and proliferation of moving compacting garbage collection does not provide enough control over placement and layout. We have proposed SHAPES, a type-driven abstract placement specification that can be integrated with object-oriented languages to enable memory optimisations. SHAPES preserves both memory and object abstraction. In this paper, we formally specify the SHAPES semantics and describe its memory safety model.

cs.PL↗

arXiv2018

Bestow and Atomic: Concurrent Programming using Isolation, Delegation and Grouping

Any non-trivial concurrent system warrants synchronisation, regardless of the concurrency model. Actor-based concurrency serialises all computations in an actor through asynchronous message passing. In contrast, lock-based concurrency serialises some computations by following a lock--unlock protocol for accessing certain data. Both systems require sound reasoning about pointers and aliasing to exclude data-races. If actor isolation is broken, so is the single-thread-of-control abstraction. Similarly for locks, if a datum is accessible outside of the scope of the lock, the datum is not governed by the lock. In this paper we discuss how to balance aliasing and synchronisation. In previous work, we defined a type system that guarantees data-race freedom of actor-based concurrency and lock-based concurrency. This paper extends this work by the introduction of two programming constructs; one for decoupling isolation and synchronisation and one for constructing higher-level atomicity guarantees from lower-level synchronisation. We focus predominantly on actors, and in particular the Encore programming language, but our ultimate goal is to define our constructs in such a way that they can be used both with locks and actors, given that combinations of both models occur frequently in actual systems. We discuss the design space, provide several formalisations of different semantics and discuss their properties, and connect them to case studies showing how our proposed constructs can be useful. We also report on an on-going implementation of our proposed constructs in Encore.

cs.PL↗

arXiv2017

Actors without Borders: Amnesty for Imprisoned State

In concurrent systems, some form of synchronisation is typically needed to achieve data-race freedom, which is important for correctness and safety. In actor-based systems, messages are exchanged concurrently but executed sequentially by the receiving actor. By relying on isolation and non-sharing, an actor can access its own state without fear of data-races, and the internal behavior of an actor can be reasoned about sequentially. However, actor isolation is sometimes too strong to express useful patterns. For example, letting the iterator of a data-collection alias the internal structure of the collection allows a more efficient implementation than if each access requires going through the interface of the collection. With full isolation, in order to maintain sequential reasoning the iterator must be made part of the collection, which bloats the interface of the collection and means that a client must have access to the whole data-collection in order to use the iterator. In this paper, we propose a programming language construct that enables a relaxation of isolation but without sacrificing sequential reasoning. We formalise the mechanism in a simple lambda calculus with actors and passive objects, and show how an actor may leak parts of its internal state while ensuring that any interaction with this data is still synchronised.

cs.PL↗

arXiv2017

Spencer: Interactive Heap Analysis for the Masses

Programming language-design and run-time-implementation require detailed knowledge about the programs that users want to implement. Acquiring this knowledge is hard, and there is little tool support to effectively estimate whether a proposed tradeoff actually makes sense in the context of real world applications. Ideally, knowledge about behaviour of "typical" programs is 1) easily obtainable, 2) easily reproducible, and 3) easily sharable. We present Spencer, a web service and API framework for dynamic analysis of a continuously growing set of traces of standard program corpora. Users do not obtain traces on their own, but can instead send queries to the web service that will be executed on a set of program traces. Queries are built in terms of a set of query combinators that present a high level interface for working with trace data. Since the framework is high level, and there is a hosted collection of recorded traces, queries are easy to implement. Since the data sets are shared by the research community, results are reproducible. Since the actual queries run on one (or many) servers that provide analysis as a service, obtaining results is possible on commodity hardware. Data in Spencer is meant to be obtained once, and analysed often, making the overhead of data collection mostly irrelevant. This allows Spencer to collect more data than traditional tracing tools can afford within their performance budget. Results in Spencer are cached, making complicated analyses that build on cached primitive queries speedy.

cs.PL↗