| 1. |
- Arvidsson, Ellen, et al.
(author)
-
Reference Capabilities for Flexible Memory Management
- 2023
-
In: Proceedings of the ACM on Programming Languages. - : Association for Computing Machinery (ACM). - 2475-1421. ; 7:OOPSLA2, s. 1363-1393
-
Journal article (peer-reviewed)abstract
- 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.
|
|
| 2. |
- Castegren, Elias, Doktor, 1987-, et al.
(author)
-
Developing a monadic type checker for an object-oriented language : An experience report
- 2019
-
In: SLE 2019 - Proceedings of the 12th ACM SIGPLAN International Conference on Software Language Engineering, co-located with SPLASH 2019. - New York, NY, USA : Association for Computing Machinery, Inc. - 9781450369817 ; , s. 184-196
-
Conference paper (peer-reviewed)abstract
- Functional programming languages are well-suited for developing compilers, and compilers for functional languages are often themselves written in a functional language. Functional abstractions, such as monads, allow abstracting away some of the repetitive structure of a compiler, removing boilerplate code and making extensions simpler. Even so, functional languages are rarely used to implement compilers for languages of other paradigms. This paper reports on the experience of a four-year long project where we developed a compiler for a concurrent, object-oriented language using the functional language Haskell. The focus of the paper is the implementation of the type checker, but the design works well in static analysis tools, such as tracking uniqueness of variables to ensure data-race freedom. The paper starts from a simple type checker to which we add more complex features, such as type state, with minimal changes to the overall initial design.
|
|
| 3. |
- Castegren, Elias, Doktor, 1987-, et al.
(author)
-
Encore : Coda
- 2023
-
In: Active Object Languages. - : Springer Nature.
-
Book chapter (peer-reviewed)abstract
- Encore is a programming language that was developed between 2014 and 2019. Encore was designed following the principle of inversion of defaults: computations are concurrent (rather than sequential) by default; data is isolated (rather than freely sharable) by default. The language worked as a seedbed for a large number of research ideas aimed at making programming with active objects safe, expressive and efficient.Encore allows active objects to share data but statically ensures the absence of data races and allows fully concurrent garbage collection. Active objects can synchronize using first-class futures, which are also used to delegate and coalesce computations across active objects. The type system also supports orchestration of intra-object parallelism, expressed using composable units of computation. Active objects which see a lot of traffic can turn themselves into passive objects protected by lock-free synchronization mechanisms to avoid performance bottle-necks, while still facilitating safe sharing and concurrent garbage collection.This paper gives an overview of these features of Encore, reflecting on lessons learned from trying to fit all of these research ideas into a single language.
|
|
| 4. |
- Palmkvist, Viktor, et al.
(author)
-
Resolvable ambiguity : Principled resolution of syntactically ambiguous programs
- 2021
-
In: CC 2021. - New York, NY, United States : ACM.
-
Conference paper (peer-reviewed)abstract
- When building a new programming language, it can be useful to compose parts of existing languages to avoid repeating implementation work. However, this is problematic already at the syntax level, as composing the grammars of language fragments can easily lead to an ambiguous grammar. State-of-the-art parser tools cannot handle ambiguity truly well: either the grammar cannot be handled at all, or the tools give little help to an end-user who writes an ambiguous program. This composability problem is twofold: (i) how can we detect if the composed grammar is ambiguous, and (ii) if it is ambiguous, how can we help a user resolve an ambiguous program? In this paper, we depart from the traditional view of unambiguous grammar design and enable a language designer to work with an ambiguous grammar, while giving users the tools needed to handle these ambiguities. We introduce the concept of resolvable ambiguity wherein a user can resolve an ambiguous program by editing it, as well as an approach to computing the resolutions of an ambiguous program. Furthermore, we present a method based on property-based testing to identify if a composed grammar is unambiguous, resolvably ambiguous, or unresolvably ambiguous. The method is implemented in Haskell and evaluated on a large set of language fragments selected from different languages. The evaluation shows that (i) the approach can handle significantly more cases of language compositions compared to approaches which ban ambiguity altogether, and (ii) that the approach is fast enough to be used in practice.
|
|
| 5. |
- Palmkvist, Viktor, et al.
(author)
-
Statically Resolvable Ambiguity
- 2023
-
In: Proceedings of the ACM on Programming Languages. - : ACM Digital Library. - 2475-1421. ; 7:POPL, s. 1686-1712
-
Journal article (peer-reviewed)abstract
- Traditionally, a grammar defining the syntax of a programming language is typically both context free and unambiguous. However, recent work suggests that an attractive alternative is to use ambiguous grammars,thus postponing the task of resolving the ambiguity to the end user. If all programs accepted by an ambiguous grammar can be rewritten unambiguously, then the parser for the grammar is said to be resolvably ambiguous. Guaranteeing resolvable ambiguity statically---for all programs---is hard, where previous work only solves it partially using techniques based on property-based testing. In this paper, we present the first efficient, practical, and proven correct solution to the statically resolvable ambiguity problem. Our approach introduces several key ideas, including splittable productions, operator sequences, and the concept of a grouper that works in tandem with a standard parser. We prove static resolvability using a Coq mechanization and demonstrate its efficiency and practical applicability by implementing and integrating resolvable ambiguity into an essential part of the standard OCaml parser.
|
|
| 6. |
- Åkerblom, Beatrice, et al.
(author)
-
Progress Report : Exploring API Design for Capabilities for Programming with Arrays
- 2019
-
In: ICOOOLPS '19. - New York, NY, USA : Association for Computing Machinery (ACM). - 9781450368629
-
Conference paper (peer-reviewed)abstract
- In on-going work, we are exploring reference capabilities for arrays, with the intention of carrying over previous results on statically guaranteed data-race freedom to parallel array algorithms. Reference capabilities typically restrict incoming pointers to an object to one (uniqueness), or restrict operations via multiple pointer to a single object (e.g., to only read). Extending such a design to arrays involve operations such as logically partitioning an array so that even though there are multiple pointers to a single array, these pointers cannot access the same elements.In this paper, we report on the on-going work of a prototype implementation of array capabilities, focusing in particular on the "array capability API design", meaning the native operations on capabilities such as splitting and merging arrays. Using our prototype implementation, we translate several existing array algorithms into using array capabilities and qualitatively study the result. In addition to identifying the need for additional operations, we study what features are commonly exercised, what are the recurring patterns, and how reliance on direct element addressing using indexes can be reduced. We end by discussing a possible design for a more performant implementation once the API is fixed.
|
|
| 7. |
- Åkerblom, Beatrice, et al.
(author)
-
Reference Capabilities for Safe Parallel Array Programming
- 2020
-
In: The Art, Science, and Engineering of Programming. - : Aspect-Oriented Software Association (AOSA). - 2473-7321. ; 4:1
-
Journal article (peer-reviewed)abstract
- 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. (edited) 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.
|
|
