title: Concurrent and parallel garbage collection for lightweight threads on multicore processors

authors:
Katsuhiro Ueno
Atsushi Ohori

abstract: This paper develops a concurrent and parallel garbage collection (GC) method that works with a lightweight thread library realizing the standard M:N threading model. The GC algorithm is organized as a set of procedures that are called from a user-level thread at various occasions and executed in the context of the OS-level threads owning the user-level thread. The procedures realize an on-the-fly collection that does not stop any thread. All OS-level threads cooperatively perform the collection in parallel. This construction achieves the same degree of parallelism as underlying lightweight thread scheduling. We have implemented the algorithm in a Standard ML compiler and have evaluated the performance with sequential and parallel benchmark programs. Our implementation shows good parallel scalability comparable to C programs directly using the lightweight threads library.


venue: ismm

title: Picking a CHERI Allocator: Security and Performance Considerations

authors:
Jacob Bramley
Dejice Jacob
Andrei Lascu
Jeremy Singer
Laurence Tratt

abstract: Several open-source memory allocators have been ported to CHERI, a hardware capability platform. In this paper we examine the security and performance of these allocators when run under CheriBSD on Arm's prototype Morello platform. We introduce a number of security attacks and show that all but one allocator are vulnerable to some of the attacks --- including the default CheriBSD allocator. We then show that while some forms of allocator performance are meaningful, comparing the performance of hybrid and pure capability (i.e. "running in non-CHERI vs. running in CHERI modes") allocators does not currently appear to be meaningful. Although we do not fully understand the reasons for this, it seems to be at least as much due to factors such as immature compiler toolchains and prototype hardware as it is due to the effects of capabilities on performance.


title: Concurrent GCs and Modern Java Workloads: A Cache Perspective

authors:
Maria Carpen-Amarie
Georgios Vavouliotis
Konstantinos Tovletoglou
Boris Grot
René Müller

abstract:
The garbage collector (GC) is a crucial component of language runtimes, offering correctness guarantees and high productivity in exchange for a run-time overhead. Concurrent collectors run alongside application threads (mutators) and share CPU resources. A likely point of contention between mutators and GC threads and, consequently, a potential overhead source is the shared last-level cache (LLC).

This work builds on the hypothesis that the cache pollution caused by concurrent GCs hurts application performance. We validate this hypothesis with a cache-sensitive Java micro-benchmark. We find that concurrent GC activity may slow down the application by up to 3× and increase the LLC misses by 3 orders of magnitude. However, when we extend our analysis to a suite of benchmarks representative for today’s server workloads (Renaissance), we find that only 5 out of 23 benchmarks show a statistically significant correlation between GC-induced cache pollution and performance. Even for these, the performance overhead of GC does not exceed 10%. Based on further analysis, we conclude that the lower impact of the GC on the performance of Renaissance benchmarks is due to their lack of sensitivity to LLC capacity.


title: Blast from the Past: Least Expected Use (LEU) Cache Replacement with Statistical History

authors:
Sayak Chakraborti
Zhizhou Zhang
Noah Bertram
Chen Ding
Sandhya Dwarkadas

abstract:
Cache replacement policies typically use some form of statistics on past access behavior. As a common limitation, however, the extent of the history being recorded is limited to either just the data in cache or, more recently, a larger but still finite-length window of accesses, because the cost of keeping a long history can easily outweigh its benefit.

This paper presents a statistical method to keep track of instruction pointer-based access reuse intervals of arbitrary length and uses this information to identify the Least Expected Use (LEU) blocks for replacement. LEU uses dynamic sampling supported by novel hardware that maintains a state to record arbitrarily long reuse intervals. LEU is evaluated using the Cache Replacement Championship simulator, tested on PolyBench and SPEC, and compared with five policies including a recent technique that approximates optimal caching using a fixed-length history. By maintaining statistics for an arbitrary history, LEU outperforms previous techniques for a broad range of scientific kernels, whose data reuses are longer than those in traces traditionally used in computer architecture studies.


title: Analyzing and Improving the Scalability of In-Memory Indices for Managed Search Engines

authors:
Aditya Chilukuri
Shoaib Akram

abstract:
Managed search engines, such as Apache Solr and Elastic- search, host huge inverted indices in main memory to offer fast response times. This practice faces two challenges. First, limited DRAM capacity necessitates search engines aggres- sively compress indices to reduce their storage footprint. Unfortunately, our analysis with a popular search library shows that compression slows down queries (on average) by up to 1.7× due to high decompression latency. Despite their performance advantage, uncompressed indices require 10× more memory capacity, making them impractical. Second, indices today reside off-heap, encouraging unsafe memory accesses and risking eviction from the page cache.

Emerging byte-addressable and scalable non-volatile mem- ory (NVM) offers a good fit for storing uncompressed indices. Unfortunately, NVM exhibits high latency. We rigorously evaluate the performance of DRAM and NVM-backed com- pressed/uncompressed indices to find that an uncompressed index in a high-capacity managed heap memory-mapped over NVM provides a 36% reduction in query response times compared to a DRAM-backed compressed index in off-heap memory. Also, it is only 11% slower than the uncompressed index in a DRAM heap (fastest approach). DRAM and NVM- backed compressed (off-heap) indices behave similarly.

We analyze the narrow response time gap between DRAM and NVM-backed indices. We conclude that inverted indices demand massive memory capacity, but search algorithms exhibit a high spatial locality that modern cache hierarchies exploit to hide NVM latency. We show the scalability of uncompressed indices on the NVM-backed heap with large core counts and index sizes. This work uncovers new space- time tradeoffs in storing in-memory inverted indices.


title: Memory Consistency Models for Program Transformations: An Intellectual Abstract

authors:
Akshay Gopalakrishnan
Clark Verbrugge
Mark Batty

abstract: Memory consistency models traditionally specify the behavior of shared memory concurrent hardware. Hardware behavior drifts away from traditional sequential reasoning, thus exhibiting behaviors that are termed as "weak". Weaker consistency models allow for more concurrent behaviors, thus justifying hardware optimizations such as read/write buffers. In parallel, weaker memory models for software allow more compiler optimizations (transformations). However, this "more" may not be strict: certain safe optimizations in stronger models are rendered unsafe in ones weaker than them. We identify properties that must hold among a pair of weak and strong memory models to guarantee this. We propose a framework using which we could build such models, showcasing our results in allowing Read Read reordering over Sequential Consistency (SC). We also show how to partially retain our desired property for a pair of models, placing constraints on the set of transformations or equivalently, on program structure. Lastly, we discuss the potential advantage of designing models satisfying such properties.


title: Flexible and Effective Object Tiering for Heterogeneous Memory Systems

authors:
Brandon Kammerdiener
J. Zach McMichael
Michael R. Jantz
Kshitij A. Doshi
Terry R. Jones

abstract: Computing platforms that package multiple types of memory, each with their own performance characteristics, are quickly becoming mainstream. To operate efficiently, heterogeneous memory architectures require new data management solutions that are able to match the needs of each application with an appropriate type of memory. As the primary generators of memory usage, applications create a great deal of information that can be useful for guiding memory tiering, but the community still lacks tools to collect, organize, and leverage this information effectively. To address this gap, this work introduces a novel software framework that collects and analyzes object-level information to guide memory tiering. Using this framework, this study evaluates and compares the impact of a variety of data tiering choices, including how the system prioritizes objects for faster memory as well as the frequency and timing of migration events. The results, collected on a modern Intel platform with conventional DRAM as well as non-volatile RAM, show that guiding data tiering with object-level information can enable significant performance and efficiency benefits compared to standard hardware- and software-directed data tiering strategies.


title: OMRGx: Programmable and Transparent Out-of-Core Graph Partitioning and Processing

authors:
Gurneet Kaur
Rajiv Gupta

abstract: Partitioning and processing of large graphs on a single machine with limited memory is a challenge. While many custom solutions for out-of-core processing have been developed, limited work has been done on out-of-core partitioning that can be far more memory intensive than processing. In this paper we present the OMRGx system whose programming interface allows the programmer to rapidly prototype existing as well as new partitioning and processing strategies with minimal programming effort and oblivious of the graph size. The OMRGx engine transparently implements these strategies in an out-of-core manner while hiding the complexities of managing limited memory, parallel computation, and parallel IO from the programmer. The execution model allows multiple partitions to be simultaneously constructed and simultaneously processed by dividing the machine memory among the partitions. In contrast, existing systems process partitions one at a time. Using OMRGx we developed the first out-of-core implementation of the popular MtMetis partitioner. OMRGx implementations of existing GridGraph and GraphChi out-of-core processing frameworks deliver performance better than their standalone optimized implementations. The runtimes of implementations produced by OMRGx decrease with the number of partitions requested and increase linearly with the graph size. Finally OMRGx default implementation performs the best of all.


title: The Unexpected Efficiency of Bin Packing Algorithms for Dynamic Storage Allocation in the Wild: An Intellectual Abstract

authors:
Christos Panagiotis Lamprakos
Sotirios Xydis
Francky Catthoor
Dimitrios Soudris

abstract:
Two-dimensional rectangular bin packing (2DBP) is a known abstraction of dynamic storage allocation (DSA). We argue that such abstractions can aid practical purposes. 2DBP algorithms optimize their placements’ makespan, i.e., the size of the used address range. At first glance modern virtual memory systems with demand paging render makespan irrelevant as an optimization criterion: allocators commonly employ sparse addressing and need worry only about fragmentation caused within page boundaries. But in the embedded domain, where portions of memory are statically pre-allocated, makespan remains a reasonable metric.

Recent work has shown that viewing allocators as black-box 2DBP solvers bears meaning. For instance, there exists a 2DBP-based fragmentation metric which often correlates monotonically with maximum resident set size (RSS). Given the field’s indeterminacy with respect to fragmentation definitions, as well as the immense value of physical memory savings, we are motivated to set allocator-generated placements against their 2DBP-devised, makespan-optimizing counterparts. Of course, allocators must operate online while 2DBP algorithms work on complete request traces; but since both sides optimize criteria related to minimizing memory wastage, the idea of studying their relationship preserves its intellectual–and practical–interest.

Unfortunately no implementations of 2DBP algorithms for DSA are available. This paper presents a first, though partial, implementation of the state-of-the-art. We validate its functionality by comparing its outputs’ makespan to the theoretical upper bound provided by the original authors. Along the way, we identify and document key details to assist analogous future efforts.

Our experiments comprise 4 modern allocators and 8 real application workloads. We make several notable observations on our empirical evidence: in terms of makespan, allocators outperform Robson’s worst-case lower bound 93.75% of the time. In 87.5% of cases, GNU’s malloc implementation demonstrates equivalent or superior performance to the 2DBP state-of-the-art, despite the second operating offline.

Most surprisingly, the 2DBP algorithm proves competent in terms of fragmentation, producing up to 2.46x better solutions. Future research can leverage such insights towards memory-targeting optimizations.


title: ZipKV: In-Memory Key-Value Store with Built-In Data Compression

authors:
Linsen Ma
Rui Xie
Tong Zhang

abstract: This paper studies how to mitigate the speed performance loss caused by integrating block data compression into in-memory key-value (KV) stores. Despite extensive prior research on in-memory KV stores, little focus has been given to memory usage reduction via block data compression (e.g., LZ4, ZSTD) due to potential performance degradation. This paper introduces design techniques to mitigate compression-induced performance degradation by utilizing decompression streaming, latency differences between compression and decompression, and data access locality in real-world workloads. These techniques can be incorporated into conventional hash or B+-tree indexing structures, enabling integration with most in-memory KV stores without altering their core indexing data structures. For demonstration, we implemented ZipKV that incorporates the developed design techniques. Compared with RocksDB (in-memory mode) that employs the log-structured merge tree indexing data structure with natural support of block data compression, ZipKV realizes similar memory usage reduction via block data compression, reduces the point query latency by 68% (LZ4) and 58% (ZSTD), and achieves up to 3.8× (LZ4) and 2.7× (ZSTD) point query throughput.


title: Predicting Dynamic Properties of Heap Allocations using Neural Networks Trained on Static Code: An Intellectual Abstract

authors:
Christian Navasca
Martin Maas
Petros Maniatis
Hyeontaek Lim
Guoqing Harry Xu

abstract:
Memory allocators and runtime systems can leverage dynamic properties of heap allocations – such as object lifetimes, hotness or access correlations – to improve performance and resource consumption. A significant amount of work has focused on approaches that collect this information in performance profiles and then use it in new memory allocator or runtime designs, both offline (e.g., in ahead-of-time compilers) and online (e.g., in JIT compilers). This is a special instance of profile-guided optimization.

This approach introduces significant challenges: 1) The profiling oftentimes introduces substantial overheads, which are prohibitive in many production scenarios, 2) Creating a representative profiling run adds significant engineering complexity and reduces deployment velocity, and 3) Profiles gathered ahead of time or during the warm-up phase of a server are often not representative of all workload behavior and may miss important corner cases.

In this paper, we investigate a fundamentally different approach. Instead of deriving heap allocation properties from profiles, we explore the ability of neural network models to predict them from the statically available code. As an intellectual abstract, we do not offer a conclusive answer but describe the trade-off space of this approach, investigate promising directions, motivate these directions with data analysis and experiments, and highlight challenges that future work needs to overcome.


title: Scaling Up Performance of Managed Applications on NUMA Systems

authors:
Orion Papadakis
Andreas Andronikakis
Nikos Foutris
Michail Papadimitriou
Athanasios Stratikopoulos
Foivos S. Zakkak
Polychronis Xekalakis
Christos Kotselidis

abstract:
Scaling up the performance of managed applications on Non-Uniform Memory Access (NUMA) architectures has been a challenging task, as it requires a good understanding of the underlying architecture and managed runtime environments (MRE). Prior work has studied this problem from the scope of specific components of the managed runtimes, such as the Garbage Collectors, as a means to increase the NUMA awareness in MREs.

In this paper, we follow a different approach that complements prior work by studying the behavior of managed applications on NUMA architectures during mutation time. At first, we perform a characterization study that classifies several Dacapo and Renaissance applications as per their scalability-critical properties. Based on this study, we propose a novel lightweight mechanism in MREs for optimizing the scalability of managed applications on NUMA systems, in an application-agnostic way. Our experimental results show that the proposed mechanism can result in relative performance ranging from 0.66x up to 3.29x, with a geometric mean of 1.11x, against a NUMA-agnostic execution.


title: Wait-Free Weak Reference Counting

authors:
Matthew J. Parkinson
Sylvan Clebsch
Ben Simner

abstract:
Reference counting is a common approach to memory management. One challenge with reference counting is cycles that prevent objects from being deallocated. Systems such as the C++ and Rust standard libraries introduce two types of reference: strong and weak. A strong reference allows access to the object and prevents the object from being deallocated, while a weak reference only prevents deallocation. A weak reference can be upgraded to provide a strong reference provided there are other strong references to the object. Hence, the upgrade operation is partial, and may fail dynamically. The classic implementation of this upgrade operation is not wait-free, that is, it can take arbitrarily long to complete if there is contention on the reference count.

In this paper, we propose a wait-free algorithm for weak reference counting. The algorithm requires primitive wait- free atomic operations of “compare and swap”, and “fetch and add”. We provide a correctness proof of the algorithm using the Starling verification tool. We provide a full implementation in C++ and demonstrate the best and worst case performance using micro-benchmarks. For our best case scenario with high contention, our new algorithm provides ~3x more throughput, while for the worst case the new algorithm is ~85% slower. Based on a worst case analysis, we provide a second algorithm that combines the strengths of the two algorithms, and has a significantly improved worst case with ~30% overhead, while maintaining the ~3x speedup for the best case.


title: NUMAlloc: A Faster NUMA Memory Allocator

authors:
Hanmei Yang
Xin Zhao
Jin Zhou
Wei Wang
Sandip Kundu
Bo Wu
Hui Guan
Tongping Liu

abstract: The NUMA architecture accommodates the hardware trend of an increasing number of CPU cores. It requires the cooperation of memory allocators to achieve good performance for multithreaded applications. Unfortunately, existing allocators do not support NUMA architecture well. This paper presents a novel memory allocator – NUMAlloc, that is designed for the NUMA architecture. is centered on a binding-based memory management. On top of it, proposes an “origin-aware memory management” to ensure the locality of memory allocations and deallocations, as well as a method called “incremental sharing” to balance the performance benefits and memory overhead of using transparent huge pages. According to our extensive evaluation, NUMAlloc has the best performance among all evaluated allocators, running 15.7% faster than the second-best allocator (mimalloc), and 20.9% faster than the default Linux allocator with reasonable memory overhead. NUMAlloc is also scalable to 128 threads and is ready for deployment.


title: The One Pass (OP) Compactor: An Intellectual Abstract

authors:
Tomer Cory
Erez Petrank

abstract: Compaction algorithms alleviate fragmentation by relocating heap objects to compacted areas. A full heap compaction eliminates fragmentation by compacting all objects into the lower addresses of the heap. Following a marking phase that marks all reachable (live) objects, the compactor needs to copy all marked objects to the beginning of the address space and fix all pointers to reference the new object locations. Initially, this process required three heap passes (beyond the marking phase). However, modern algorithms, culminating in the Compressor, have reduced this cost to a single heap pass plus a single pass over an auxiliary table, that is smaller than (yet proportional to) the size of the heap. In this paper, we introduce the One Pass (OP) Compactor: a novel combination of existing compactors that reduces the complexity of compaction to a single heap pass. This represents arguably the best possible complexity for a compaction algorithm. Additionally, we extend the OP compactor with a parallel version, enabling scalability on a multicore platform. This paper is classified as an intellectual abstract because it introduces the new algorithm but does not provide an accompanying implementation and evaluation.


title: BatchIt: Optimizing Message-Passing Allocators for Producer-Consumer Workloads: An Intellectual Abstract

authors:
Nathaniel Wesley Filardo
Matthew J. Parkinson

abstract: Modern, high-performance memory allocators must scale to a wide array of uses, including producer-consumer workloads. In such workloads, objects are allocated by one thread and deallocated by another, which we call remote deallocations. These remote deallocations lead to contention on the allocator’s synchronization mechanisms. Message-passing allocators, such as mimalloc and snmalloc, use message queues to communicate remote deallocations between threads. These queues work well for producer-consumer workloads, but there is room for optimization. We propose and characterize BatchIt, a conceptually simple optimization for such allocators: a per-slab cache of remote deallocations that enables batching of objects destined for the same slab. This optimization aims to exploit naturally-arising locality of allocations, and it generalizes across particular implementations; we have implementations for both mimalloc and snmalloc. Multi-threaded, producer-consumer benchmarks show improved performance from reduced rates of atomic operations and cache misses in the underlying allocator. Experimental results using the mimalloc-bench suite and a custom message-passing workload show that some producer-consumer workloads see over 20% performance improvement even atop the high performance these allocators already provide.


title: Supporting Trusted Virtual Machines with Hardware-Based Secure Remote Memory

authors:
Taekyung Heo
Seunghyo Kang
Sanghyeon Lee
Soojin Hwang
Joongun Park
Jaehyuk Huh

abstract: Although recent studies have been improving the performance of RDMA-based memory disaggregation systems, their security aspect has not been thoroughly investigated. For secure disaggregated memory, the memory-providing node must protect its memory from memory-requesting nodes, and the memory-requesting node requires the confidentiality and integrity protection of its memory contents in the remote node, even when the privileged software is compromised. To provide protection of remote memory, this study proposes a hardware-assisted memory disaggregation system. The proposed trusted disaggregated memory combines the current trusted hardware-based virtual machine (VM) and a new dedicated hardware engine for trusted memory disaggregation. The processor with supports for trusted VM protects the context of a user VM within the local system, while the proposed hardware engine provides an efficient isolation and protection of remote memory pages, guaranteeing the confidentiality and integrity of remote memory pages. In the secure memory disaggregation system, fast address translation and access validation are supported with the cooperation of the hardware engine and guest OS in a trusted virtual machine. In addition, the proposed system hides the memory access patterns observable from remote nodes, supporting obliviousness. Our evaluation with an FPGA-based prototype implementation shows that such fine-grained secure disaggregated memory is feasible with comparable performance to the latest software-based technique without security support.


title: A Heuristic for Periodic Memory Allocation with Little Fragmentation to Train Neural Networks

authors:
Akifumi Imanishi
Zijian Xu

abstract: Neural network training requires immense GPU memory, and memory optimization methods such as recomputation are being actively researched. Recent improvements in recomputation have reduced more than 90 % of the peak allocated size. However, because it produces complex irregular allocation patterns, PyTorch’s default caching allocator wastes up to 20 % of memory because of severe fragmentation and increases the cache management overhead. The periodic allocation patterns during training make offline memory optimization possible. Dynamic storage allocation (DSA) is the problem of minimizing the memory address ranges given the allocation pattern. This is defined as the 2D bin-packing problem, in which each rectangle can move only vertically. Although the first-fit or best-fit heuristics perform well for DSA, we propose a simulated annealing-based non-trivial heuristic algorithm that optimizes the topological ordering of allocations to further minimize fragmentation. The proposed algorithm evaluates a candidate allocation plan with O(logN) amortized time, where N is the number of allocations. We empirically tested our algorithm on both randomly generated data and allocation patterns obtained by training popular vision and text models with recomputation. The experiments showed that, on average, our algorithm reduced fragmentation caused by the PyTorch caching allocator from 29.5 % to 0.4 %, compared to 5.3 % by the first-fit method.


title: A Managed Memory System for Micro Controllers with NOR Flash Memory

authors:
Akira Inoue
Tomoharu Ugawa
Shigeru Chiba

abstract: This paper presents a managed memory system for micro controllers with only a small amount of memory but with NOR flash memory. This system is targeted at a device such as Raspberry Pi Pico, which is equipped with ARM Coretex M0+, on-chip 264KB SRAM, and 2MB flash memory. To extend an available memory space for user programs, this system provides virtual memory by using NOR flash memory as a backing store. Since writing data to the flash memory is slow and the number of writes is limited during its lifetime, this system cooperates language-level memory management to mitigate these drawbacks. It runs a garbage collector that may move objects aggressively when a memory page is paged-out to flash memory. This paper also proposes a technique named a forwarding bit to efficiently implement the movement of objects stored in flash memory. According to experiments using a prototype of this system implemented for the mruby language on Raspberry Pi Pico, when the available SRAM size is small, this system successfully reduces the number of erasures in flash memory to an average of less than 10% and even improves execution speed by an average of 4 times faster despite overhead of moving objects.


title: Evaluating Finalization-Based Object Lifetime Profiling

authors:
Sebastian Jordan-Montaño
Guillermo Polito
Stéphane Ducasse
Pablo Tesone

abstract: Using object lifetime information enables performance improvement through memory optimizations such as pretenuring and tuning garbage collector parameters. However, profiling object lifetimes is nontrivial and often requires a specialized virtual machine to instrument object allocations and dereferences. Alternative lifetime profiling could be done with less implementation effort using available finalization mechanisms such as weak references. In this paper, we study the impact of finalization on object lifetime profiling. We built an actionable lifetime profiler using the ephemeron finalization mechanism named FiLiP. FiLiP instruments object allocations to exactly record an object’s allocation time and it attaches an ephemeron to each allocated object to capture its finalization time. We show that FiLiP can be used in practice and achieves a significant overhead reduction by pretenuring the ephemeron objects. We further experiment with the impact of sampling object allocations, showing that sampling further reduces profiling overhead while still maintaining actionable lifetime measurements.


title: Garbage Collection for Mostly Serialized Heaps

authors:
Chaitanya S. Koparkar
Vidush Singhal
Aditya Gupta
Mike Rainey
Michael Vollmer
Artem Pelenitsyn
Sam Tobin-Hochstadt
Milind Kulkarni
Ryan R. Newton

abstract: Over the years, traditional tracing garbage collectors have accumulated assumptions that may not hold in new language designs. For instance, we usually assume that run-time objects do not hold addressable sub-parts and have a size of at least one pointer. These fail in systems striving to eliminate pointers and represent data in a dense, serialized form, such as the Gibbon compiler. We propose a new memory management strategy for language runtimes with mostly serialized heaps. It uses a hybrid, generational collector, where regions are bump-allocated into the young generation and objects are bump-allocated within those regions. Minor collections copy data into larger regions in the old generation, compacting it further. The old generation uses region-level reference counting. The resulting system maintains high performance for data traversal programs, while significantly improving performance on other kinds of allocation patterns.


title: Reference Counting Deeply Immutable Data Structures with Cycles: An Intellectual Abstract

authors:
Matthew J. Parkinson
Sylvan Clebsch
Tobias Wrigstad

abstract: Immutable data structures are a powerful tool for building concurrent programs. They allow the sharing of data without the need for locks or other synchronisation mechanisms. This makes it much easier to reason about the correctness of the program. In this paper, we focus on what we call deep immutability from freeze, that is, objects are initially mutable, and then can be frozen, and from that point on the object and everything it refers to (transitively) can no longer be mutated. A key challenge with this form of immutability is “how to manage the memory of cyclic data structures?” The standard approach is to use a garbage collector (GC), or a back-up cycle detector. These approaches sacrifice the promptness of memory reclamation, and the determinism of memory usage. In this paper, we argue that memory underlying an immutable data structure can be efficiently managed using reference counting even in the presence of cycles, based on the observation that the cycles are themselves immutable. Our approach takes a classic algorithm for calculating strongly connected components (SCCs) and managing equivalence classes with union-find (UF), and combines them so that the liveness of each SCC can be tracked efficiently using only a single reference counter. The key observation is that since the graph is unchanging, we can calculate the SCCs once, in time that is almost linear in the size of the graph, and then use the result to reference count at the level of the SCCs. This gives precise reachability information, and does not require any backup mechanism to detect or handle cycles.


title: Memory Management on Mobile Devices

authors:
Kunal Sareen
Stephen M. Blackburn
Sara S. Hamouda
Lokesh Gidra

abstract:
The performance of mobile devices directly affects billions of people worldwide. Yet, despite memory management being key to their responsiveness, energy efficiency, and cost, mobile devices are understudied in the literature. A paucity of suitable methodologies and benchmarks is likely both a cause and a consequence of this gap. It also reflects the challenges of evaluating mobile devices due to: i) their inherently multi-tenanted nature, ii) the scarcity of widely-used open source workloads suitable as benchmarks, iii) the challenge of determinism and reproducibility given mobile devices' extensive use of GPS and network services, iv) the complexity of mobile performance criteria.

We study this problem using the Android Runtime (ART), which is particularly interesting because it is open sourced, garbage collected, and its market extends from the most advanced to the most basic mobile devices available, with a commensurate diversity of performance expectations. Our study makes the following contributions: i) we identify pitfalls and challenges to the sound evaluation of garbage collection in ART, ii) we describe a framework for the principled performance evaluation of overheads in ART, iii) we curate a small benchmark suite comprised of widely-used real-world applications, and iv) we conduct an evaluation of these real-world workloads as well as some DaCapo benchmarks and a micro-benchmark. For a modestly sized heap, we find that the lower bound on garbage collection overheads vary considerably among the benchmarks we evaluate, from 2 % to 51 %, and that overall, overheads are similar to those identified in recent studies of Java workloads running on OpenJDK. We hope that this work will demystify the challenges of studying memory management in the Android Runtime. By doing so, we hope to open up research and lead to more innovation in this highly impactful and memory-sensitive domain.


title: ESPN: Memory-Efficient Multi-vector Information Retrieval

authors:
Susav Shrestha
A. L. Narasimha Reddy
Zongwang Li

abstract: Recent advances in large language models have demonstrated remarkable effectiveness in information retrieval (IR) tasks. While many neural IR systems encode queries and documents into single-vector representations, multi-vector models elevate the retrieval quality by producing multi-vector representations and facilitating similarity searches at the granularity of individual tokens. However, these models significantly amplify memory requirements for retrieval indices by an order of magnitude. This escalation in index size renders the scalability of multi-vector IR models progressively challenging due to their substantial memory demands. We introduce Embedding from Storage Pipelined Network (ESPN) where we offload the entire re-ranking embedding tables to SSDs and reduce the memory requirements by 5−16×. We design a flexible software prefetcher applicable to any hierarchical clustering based search, achieving hit rates exceeding 90%. ESPN improves SSD based retrieval up to 6.4× and end-to-end throughput by 68% to maintain near-memory levels of query latency even for large query batch sizes. The code is available at https://github.com/susavlsh10/ESPN-v1.


title: SSRD: Shapes and Summaries for Race Detection in Concurrent Data Structures

authors:
Xiaofan Sun
Rajiv Gupta

abstract: Concolic testing combines concrete execution with symbolic execution to automatically generate test inputs that exercise different program paths and deliver high code coverage. This approach has been extended to multithreaded programs for exposing data races. Multithreaded programs frequently rely upon concurrent dynamic data structures whose implementations may contain data races that manifest only when certain dynamic data structure shapes, program paths, and thread interleavings are exercised. The lack of support for exploring different data structure shapes compromises the detection of races. This paper presents a summarization-guided approach for concolic testing capable of efficiently exploring different dynamic data structure shapes to expose data races. Via unit testing of key functions, function summaries are generated that capture data structure shapes that cause various function paths to be exercised. The shapes are captured in the form of pointer-pointee relations among symbolic pointers. By reusing function summaries during concolic testing, much of the overhead of handling symbolic pointers and dynamic objects in summarized functions is avoided. The summary also contains symbolic memory accesses and synchronization events that guide application-level concolic testing first to identify and then confirm potential data races. We demonstrate the efficiency and efficacy of our approach via experiments with multithreaded programs performing concurrent operations on four widely used dynamic data structures - Skip List, Unrolled Linked List, Priority Queue, and AVL Tree. It increases the number of races detected from 34 to 74 in total in comparison to Cloud9, and reduces both constraints solving time and number of constraints needed to be solved via summarization.


title: Reconsidering Garbage Collection in Julia: A Practitioner Report

authors:
Luís Eduardo de Souza Amorim
Yi Lin
Stephen M. Blackburn
Diogo Netto
Gabriel Baraldi
Nathan Daly
Antony L. Hosking
Kiran Pamnany
Oscar Smith

abstract: Julia is a dynamically-typed garbage-collected language designed for high performance. Julia has a non-moving tracing collector, which, while performant, is subject to the same unavoidable fragmentation and lack of locality as all other non-moving collectors. In this work, we refactor the Julia runtime with the goal of supporting different garbage collectors, including copying collectors. Rather than integrate a specific collector implementation, we implement a third-party heap interface that allows Julia to work with various collectors, and use that to implement a series of increasingly more advanced designs. Our description of this process sheds light on Julia's existing collector and the challenges of implementing copying garbage collection in a mature, high-performance runtime. We have successfully implemented a third-party heap interface for Julia and demonstrated its utility through integration with the MMTk garbage collection framework. We hope that this account of our multi-year effort will be useful both within the Julia community and the garbage collection research community, as well as providing insights and guidance for future language implementers on how to achieve high-performance garbage collection in a highly-tuned language runtime.


title: Lifetime Dispersion and Generational GC: An Intellectual Abstract

abstract:
The effectiveness of generational garbage collection is usually explained through the generational hypothesis, that “most objects die young”.

Despite its simplicity, the generational hypothesis leaves some things to be desired: it is not obvious how it can be measured as a property of a program (independent of a particular GC strategy), it is not composable (in that it does not follow from a larger program by being true of its parts), and even its connection to the effectiveness of generational GC is murkier than it may first appear.

We propose instead lifetime dispersion as a measure of how generational a program’s objects are, and explain how it can be quantified by the Gini coefficient. We show that this measure is both composable, and directly connected to effectiveness of generational collection.


title: EMD: Fair and Efficient Dynamic Memory De-bloating of Transparent Huge Pages

authors:
Parth Gangar
Ashish Panwar
K. Gopinath

abstract: Recent processors rely on huge pages to reduce the cost of virtual-to-physical address translation. However, huge pages are notorious for creating memory bloat – a phenomenon wherein the OS ends up allocating more physical memory to an application than its actual requirement. This extra memory can be reclaimed by the OS via de-bloating at runtime. However, we find that current OS-level solutions either lack support for dynamic memory de-bloating, or suffer from performance and fairness pathologies while de-bloating. We address these issues with EMD (Efficient Memory De-bloating). The key insight in EMD is that different regions in an application’s address space exhibit different amounts of memory bloat. Consequently, the tradeoff between memory efficiency and performance varies significantly within a given application e.g., we find that memory bloat is typically concentrated in specific regions, and de-bloating them leads to minimal performance impact. Hinged on this insight, EMD employs a prioritization scheme for fine-grained, efficient, and fair reclamation of memory bloat. EMD improves performance by up to 69% compared to HawkEye — a state-of-the-art OS-based huge page management system. EMD also eliminates fairness concerns associated with dynamic memory de-bloating.


title: Arborescent Garbage Collection: A Dynamic Graph Approach to Immediate Cycle Collection

authors:
Frédéric Lahaie-Bertrand
Léonard Oest O'Leary
Olivier Melançon
Marc Feeley
Stefan Monnier

abstract:
Reclaiming cyclic garbage has been a long-standing challenge in automatic memory management. Common approaches to this problem often involve extending reference counting with an asynchronous background task to reclaim cycles. While this ensures that cycles are eventually collected, it also introduces unpredictable behaviours, making these approaches unsuitable for applications where deterministic collection is required.

This paper introduces Arborescent Garbage Collection, a synchronous memory management algorithm that immediately reclaims unreachable memory objects, including cyclic structures. Inspired by single-source reachability algorithms on dynamic graphs, it extends the idea of embedding a spanning forest in a program's reference graph to track the reachability of any object from a root. When a reference is removed, the algorithm efficiently rebuilds the forest and immediately reclaims the memory of objects that are no longer reachable. The result is a garbage collection algorithm suitable for applications that require immediate memory reclamation and predictable behaviour.


title: Gray-in-Young: A Generational Garbage Collection for Processing-in-Memory

authors:
Ryu Morimoto
Kazuki Ichinose
Tomoharu Ugawa

abstract: Processing-in-memory (PIM) is a promising approach to overcome the performance bottleneck caused by the gap between CPU speed and memory speed, known as the memory wall problem. The UPMEM PIM-enabled memory is the first commercialized general-purpose PIM accelerator, to which the program running on the host CPU offloads computation kernels. Its DRAM Processing Units (DPUs) are general-purpose processors and have the flexibility to run various computation kernels. However, there is no support for programming in managed languages with garbage collection (GC). In this paper, we design GC for DPUs, which is a key component of managed runtimes. Our GC is a parallel generational GC, whose young space is in scratch pad memory (SPM). The GC updates pointers in promoting objects before copying them to old space in DRAM to reduce DRAM accesses. It also determines class information needed for minor GC of each computation kernel at compile time and caches them in SPM. The major GC routines are compiled in a separate binary so that the binaries of computation kernels fit in 24 KB of program memory. The evaluation results using a micro benchmark showed that our proposed techniques reduced up to 85.9% DRAM accesses and improved performance by 46.2% for our benchmark. The GC scaled up to 11 threads, and the remaining code size for the GC routine was only 4.3 KB after separating 6.9 KB of major GC.


title: Fully Randomized Pointers

authors:
Sai Dhawal Phaye
Gregory J. Duck
Roland H. C. Yap
Trevor E. Carlson

abstract:
Memory errors continue to be a critical concern for programs written in low-level programming languages such as C and C++. Many different memory error defenses have been proposed, each with varying trade-offs in terms of overhead, compatibility, and attack resistance. Some defenses are highly compatible but only provide minimal protection, and can be easily bypassed by knowledgeable attackers. On the other end of the spectrum, capability systems offer very strong (unforgeable) protection, but require novel software and hardware implementations that are incompatible by definition. The challenge is to achieve both very strong protection and high compatibility.

In this paper, we propose Fully Randomized Pointers (FRP) as a strong memory error defense that also maintains compatibility with existing binary software. The key idea behind FRP is to design a new pointer encoding scheme that allows for the full randomization of most pointer bits, rendering even brute force attacks impractical. We design a FRP encoding that is: (1) compatible with existing binary code (recompilation not needed); and (2) decoupled from the underlying object layout. FRP is prototyped as: (i) a software implementation (BlueFat) to test security and compatibility; and (ii) a proof-of-concept hardware implementation (GreenFat) to evaluate performance. We show FRP is secure, practical, and compatible at the binary level, while our hardware implementation achieves low performance overheads (<4%).


title: Compiler-Assisted Crash Consistency for PMEM

authors:
Yun Joon Soh
Sihang Liu
Steven Swanson
Jishen Zhao

abstract:
Writing crash-consistent programs for memory-semantic storage such as persistent memory (PMEM) is error-prone and cumbersome. Programmers must implement both the main logic and the recovery logic to ensure data consistency after unexpected power failures. Prior work has reduced this burden using compiler-assisted logging techniques to enforce crash consistency. However, these techniques often apply persistence uniformly, limiting support for diverse programming models and incurring high logging overhead.

We present SSAPP (Statically and Systematically Automated Persistence is Possible), a compiler extension that transparently adds crash consistency to the main logic and automatically generates tailored recovery code. SSAPP persists transient state with low overhead during main logic execution and makes principled resumption decisions during post-failure recovery. Based on these decisions, the generated recovery code correctly completes the interrupted operation. This design supports a broader range of programming models — including lock-free data structures — while reducing crash consistency overhead.

We evaluate SSAPP on transactional benchmarks, lock-based, and lock-free data structures. With minimal developer effort, SSAPP converts volatile lock-free data structures into crash-consistent ones, achieving performance comparable to Mirror, a hand-optimized persistent data structure library. SSAPP also outperforms Clobber-NVM, a prior compiler-based PMEM system, achieving 1.8× higher throughput.


title: TierTrain: Proactive Memory Tiering for CPU-Based DNN Training

authors:
Sathvik Swaminathan
Sandeep Kumar
Aravinda Prasad
Sreenivas Subramoney

abstract:
Deep neural networks (DNNs) are one of the popular models for learning relationships between complex data. Training a DNN model is a compute- and memory-intensive operation. The size of modern DNN models spans into the terabyte region, requiring multiple accelerators to train -- driving up the training cost. Such humongous memory requirements shift the focus toward memory rather than computation.

CPU-memory, on the other hand, can be scaled to several terabytes with new emerging memory technologies such as HBM and CXL-attached memories. Furthermore, recent advancements to the CPUs in terms of dedicated instructions for DNN training and inference are bridging the compute gap between CPUs and accelerators.

Proposed is an exploratory work in the direction of cost-effective DNN training on CPUs where we aim to alleviate memory management challenges in DNN training. We propose TierTrain, a novel memory tiering solution based on a dynamic queuing system that leverage the periodic and deterministic memory access behavior in DNN training to manage data placement across memory tiers. TierTrain proactively manages tensors by aggressively offloading them to slow memory tiers (NVMM, CXL) and timely prefetching them back to fast memory tiers (HBM, DRAM). Our evaluation of TierTrain on a tiered memory system with a real CXL-attached memory used for memory expansion and NVMM as a low cost memory results in average fast memory footprint reduction of 59–83% and peak fast memory footprint reduction of 25–74% with a performance overhead of 1–16%. In a memory-constrained scenario, TierTrain outperforms the state-of-the-art tiering by improving the performance by 35–84% for a set of popular DNN training models.


title: Reworking Memory Management in CRuby: A Practitioner Report

authors:
Kunshan Wang
Stephen M. Blackburn
Peter Zhu
Matthew Valentine-House

abstract:
Ruby is a dynamic programming language that was first released in 1995 and remains heavily used today. Ruby underpins Ruby on Rails, one of the most widely deployed web application frameworks. The scale at which Rails is deployed has placed increasing pressure on the underlying CRuby implementation, and in particular its approach to memory management. CRuby implements a mark-sweep garbage collector which until recently was non-moving and only allocated fixed-size 40-byte objects, falling back to malloc to manage all larger objects.

This paper reports on a multi-year academic-industrial collaboration to rework CRuby's approach to memory management with the goal of introducing modularity and the ability to incorporate modern high performance garbage collection algorithms. This required identifying and addressing deeply ingrained assumptions across many aspects of the CRuby runtime. We describe the longstanding CRuby implementation and enumerate core challenges we faced and lessons they offer.

Our work has been embraced by the Ruby community, and the refactorings and new garbage collection interface we describe have been upstreamed.

We look forward to this work being used to deploy a new class of garbage collectors for Ruby. We hope that this paper will provide important lessons and insights for Ruby developers, garbage collection researchers and language designers.


title: SecureMind: A Framework for Benchmarking Large Language Models in Memory Bug Detection and Repair

authors:
Huanting Wang
Dejice Jacob
David Kelly
Yehia Elkhatib
Jeremy Singer
Zheng Wang

abstract: Large language models (LLMs) hold great promise for automating software vulnerability detection and repair, but ensuring their correctness remains a challenge. While recent work has developed benchmarks for evaluating LLMs in bug detection and repair, existing studies rely on hand-crafted datasets that quickly become outdated. Moreover, systematic evaluation of advanced reasoning-based LLMs using chain-of-thought prompting for software security is lacking. We introduce SecureMind, an open-source framework for evaluating LLMs in vulnerability detection and repair, focusing on memory-related vulnerabilities. SecureMind provides a user-friendly Python interface for defining test plans, which automates data retrieval, preparation, and benchmarking across a wide range of metrics. Using SecureMind, we assess 10 representative LLMs, including 7 state-of-the-art reasoning models, on 16K test samples spanning 8 Common Weakness Enumeration (CWE) types related to memory safety violations. Our findings highlight the strengths and limitations of current LLMs in handling memory-related vulnerabilities.


title: Enabling Huge Pages for Real-World Executables

abstract: While huge pages can dramatically reduce address translation overhead, their use for executable code remains limited by structural barriers in binary formats, page cache management, and loader mechanisms. Existing solutions copy code into anonymous memory, abandoning file-backed semantics and breaking cross-process sharing, memory reclamation, and debugging tools. Emerging kernel support for file-backed huge pages remains insufficient without relinking and modifying loaders, impractical for deployed and closed-source software.


title: Going Where No GC Has Gone Before: A No-Tradeoff Memory System for Bosque

authors:
Anthony Arnold
Mark Marron

abstract: Garbage Collectors (GCs) are a critical component of a modern application stack. Long pauses, large memory consumption, and high CPU usage can unexpectedly occur with certain workloads or series of events. These behaviors can make systems unresponsive, make it impossible to run them in resource-constrained environments, and are often very difficult to debug and fix – as their appearance may be intermittent. In fact recent theoretical work has shown what, for existing mainstream languages, these issues are unavoidable and, regardless of the GC design or implementation, there will always be workloads that cause them to occur!


title: Consistency and Coherence of the NVIDIA Grace-Hopper Superchip

authors:
Soham Bagchi
Sanya Srivastava
Reese Levine
Tyler Sorensen
Ryan Stutsman
Vijay Nagarajan

abstract: Modern heterogeneous processors like the NVIDIA Grace-Hopper Superchip tightly integrate CPU and GPU cores across a cache-coherent interconnect, with an implicit assumption that independently compiled CPU and GPU code can safely interact via shared memory. Yet the memory consistency and coherence of such systems remain empirically unvalidated. This paper presents the first systematic study of consistency and coherence on the Grace-Hopper. We empirically validate that the system enforces the Compound Memory Consistency Model (CMCM)---a theoretical prerequisite for correct independent compilation---using a novel heterogeneous litmus testing methodology spanning 1,960 test variants. We further introduce Value Propagation tests to reverse-engineer the underlying coherence mechanisms, revealing that internal GPU coherence relies on write-throughs and self-invalidations rather than classical writer-initiated invalidations, while global CPU-GPU coherence is maintained via directory-based invalidations consistent with an AMBA CHI-like protocol. These results establish the CMCM as a concrete architectural target for heterogeneous systems and provide the first empirical characterization of GPU and CPU-GPU coherence mechanisms in a commercial heterogeneous processor.


title: Stretch: A Fault-Driven DSM Runtime for Distributed Multithreaded Applications

authors:
Edoardo D'Alessio
Mohamed Husain Noor Mohamed
Xiaoguang Wang
Binoy Ravindran

abstract: Recent Linux memory-management interfaces make it practical to revisit distributed shared memory (DSM) as a deployable runtime substrate for conventional multithreaded software. We present Stretch, a userspace fault-driven page-granularity DSM runtime that combines userfaultfd-based fault interception, centralized MSI-style coherence (i.e., Modified, Shared, or Invalid), and CRIU-based thread placement to extend a process across multiple machines. Missing-page and write-protection faults are translated into fetch, invalidation, and ownership-transfer operations, while distributed barriers and coarse-grained mutexes reuse the same mechanism. Stretch supports both automatic tracking of anonymous regions and an explicit tracked-region mode that focuses coherence on genuinely shared memory.


title: Interpreter Memory Safety via Differential Fuzzing with a CHERI on Top

authors:
Kai Feng
Huanting Wang
Jeremy Singer
Zheng Wang

abstract: Memory safety is a critical issue in embedded systems. Although high-level languages like MicroPython simplify IoT development, their C-based runtimes remain vulnerable to memory errors triggered by Python code or native extensions. The CHERI (Capability Hardware Enhanced RISC Instructions) architecture offers hardware-enforced memory safety, but its effectiveness for exposing latent bugs in real-world interpreters has not yet been fully explored. We present diffCHERI:FruitFly, a novel differential testing framework for systematically uncovering memory defects in MicroPython across conventional (x86/ARM) and CHERI-enabled (Arm Morello) platforms. We mine historic vulnerabilities from diverse Python runtimes to extract recurring stress patterns, then use a large language model to generate new test programs, and apply Concrete Syntax Tree (CST) mutation to diversify inputs.


title: Reconsidering "Reconsidering Custom Memory Allocation"

authors:
Nicolas van Kempen
Emery D. Berger

abstract: Programmers using native languages such as C, C++, or Rust can implement custom memory allocation strategies to improve execution time. In their paper titled "Reconsidering Custom Memory Allocation" almost 25 years ago, Berger et al. showed that while per-class allocators provide no significant speedups over a state-of-the-art general-purpose allocator, region-based allocators can improve execution time by allocating and freeing objects in bulk. This paper revisits that work on a modern hardware platform with modern general-purpose allocators to evaluate whether their conclusions still hold. It also augments the benchmark suite with two large real-world applications (Clang and Blender), and introduces a methodology to explore the effect of memory fragmentation on locality in general-purpose allocators. Our results support and extend the original conclusions, demonstrating the locality advantages of region-based custom memory allocators.


title: Much Ado about Offset Vectors

authors:
Hayley Patton
Stephen M. Blackburn

abstract: Offset-Vector Compaction (OVC) algorithms, such as the Compressor, are among the most widely deployed garbage collectors today, yet they have remained largely unexplored by the literature since the earliest algorithms were published two decades ago. Although an implementation in the Android Runtime is publicly available and a number of other variations on the algorithm have been developed or proposed, these have not been analyzed or evaluated with recent benchmarks or compared with modern server collectors. This gap in the literature may curtail innovation and exploration of new ideas while reinforcing unchallenged conventional wisdom.


title: Stride-Aware Page Prefetching for GPU Unified Memory via Markov Pattern Prediction

authors:
Yunqi Shen
Dimitrios Nikolopoulos

abstract: GPU unified memory simplifies programming by automatically migrating pages between CPUs and GPUs, but page faults trigger migrations with hundreds of microseconds to millisecond-scale latency, stalling thousands of threads. We target this bottleneck with a page prefetching framework that predicts future faults by modeling stride (delta) transitions in addition to addresses. Across GPU workloads, we observe that while individual fault addresses may be unique, the sequence of strides between them exhibits strong regularity, including recurring multi-step and oscillatory patterns.


title: Bandwidth Speaks, We Listen: Dynamic Memory Interleaving for Tiering

authors:
Bijan Tabatabai
Eishan Mirakhur
Ravi Shankar Jonnalagadda
Vinicius Petrucci
Rohit Sehgal
Jus Singh
Michael M. Swift

abstract: CXL memory devices increase the memory capacity and bandwidth available to a server, at the cost of higher access latency. Prior research focused on how to make use of the expanded memory capacity provided by CXL while minimizing the impact of its higher access latency. However, most current memory management techniques to achieve this, such as memory tiering, do not make effective use of the expanded bandwidth provided by CXL memory. These techniques place frequently accessed data in local memory, so bandwidth intensive applications will saturate the local bandwidth and leave the remote bandwidth unutilized.


venue: jfp

title: Explicit Substitutions

authors:
Martín Abadi
Luca Cardelli
Pierre-Louis Curien
Jean-Jacques Lévy

abstract: Abstract The λσ-calculus is a refinement of the λ-calculus where substitutions are manipulated explicitly. The λσ-calculus provides a setting for studying the theory of substitutions, with pleasant mathematical properties. It is also a useful bridge between the classical λ-calculus and concrete implementations.


title: Introduction to Generalized Type Systems

abstract: Abstract Programming languages often come with type systems. Some of these are simple, others are sophisticated. As a stylistic representation of types in programming languages several versions of typed lambda calculus are studied. During the last 20 years many of these systems have appeared, so there is some need of classification. Working towards a taxonomy, Barendregt (1991) gives a fine-structure of the theory of constructions (Coquand and Huet 1988) in the form of a canonical cube of eight type systems ordered by inclusion. Berardi (1988) and Terlouw (1988) have independently generalized the method of constructing systems in the λ-cube. Moreover, Berardi (1988, 1990) showed that the generalized type systems are flexible enough to describe many logical systems. In that way the well-known propositions-as-types interpretation obtains a nice canonical form.


title: Self-Interpretations in lambda Calculus

abstract: Programming languages which are capable of interpreting themselves have been fascinating computer scientists. Indeed, if this is possible then a ‘strange loop’ (in the sense of Hofstadter, 1979) is involved. Nevertheless, the phenomenon is a direct consequence of the existence of universal languages. Indeed, if all computable functions can be captured by a language, then so can the particular job of interpreting the code of a program of that language. Self-interpretation will be shown here to be possible in lambda calculus. The set of λ-terms , notation Λ, is defined by the following abstract syntax where is the set {v, v′, v″, v′″,…} of variables . Arbitrary variables are usually denoted by x, y,z,… and λ -terms by M,N,L,…. A redex is a λ -term of the form that is, the result of substituting N for (the free occurrences of) x in M. Stylistically, it can be said that λ -terms represent functional programs including their input. A reduction machine executes such terms by trying to reduce them to normal form; that is, redexes are continuously replaced by their contracta until hopefully no more redexes are present. If such a normal form can be reached, then this is the output of the functional program; otherwise, the program diverges.


title: An Unsolvable Numeral System in lambda Calculus

abstract: Abstract For numeral systems in untyped λ-calculus the definability of a successor, a predecessor and a test for zero implies the definability of all recursive functions on that system. Towards a disproof of the converse statement, H. P. Barendregt and the author constructed a numeral system consisting of unsolvable λ-terms, being adequate for unary functions. Then, independently, B. Intrigila found an analogous system for all computable functions.


title: The Minout Problem

abstract: The problem of computing the smallest natural number not contained in a given set of natural numbers has a number of practical applications. Typically, the given set represents the indices of a class of objects ‘in use’ and it is required to find a ‘free’ object with smallest index. Our purpose in this article is to derive a linear-time functional program for the problem. There is an easy solution if arrays capable of being accessed and updated in constant time are available, but we aim for an algorithm that employs only standard lists. Noteworthy is the fact that, although an algorithm using lists is the result, the derivation is carried out almost entirely in the world of sets.


title: On Removing Duplicates

abstract: The function remdup (also called mkset in some functional languages) removes duplicates from a given list. The following definition of remdup is standard and leads to a quadratic time algorithm The operator (—) used in the last expression subtracts one list from another; its definition is Defined in this way remdup x returns the list of distinct elements of x in the order in which they first appear in x . In other words, the position of remdup JC as a subsequence of x is lexically the smallest among all possible solutions. Now let us change the problem and ask that remdup simply return the lexically least solution. Note the subtle difference between this version and the previous one: before, it was the position of the subsequence that was lexically the least, now it is the subsequence itself. To make the distinction clear, consider x = [1,4,2,4,3]. With the original definition remdup x returns [1,4,2,3]; the lexically least subsequence, however, is [1,2,4,3]. The question we are interested in is this: can we also find a quadratic time algorithm for the new problem? The answer turns out to be yes, but justifying it requires a bit of work.


title: Implementing the Evaluation Transformer Model of Reduction on Parallel Machines

abstract: Abstract The evaluation transformer model of reduction generalizes lazy evaluation in two ways: it can start the evaluation of expressions before their first use, and it can evaluate expressions further than weak head normal form. Moreover, the amount of evaluation required of an argument to a function may depend on the amount of evaluation required of the function application. It is a suitable candidate model for implementing lazy functional languages on parallel machines. In this paper we explore the implementation of lazy functional languages on parallel machines, both shared and distributed memory architectures, using the evaluation transformer model of reduction. We will see that the same code can be produced for both styles of architecture, and the definition of the instruction set is virtually the same for each style. The essential difference is that a distributed memory architecture has one extra node type for non-local pointers, and instructions which involve the value of such nodes need their definitions extended to cover this new type of node. To make our presentation accessible, we base our description on a variant of the well-known G-machine, an abstract machine for executing lazy functional programs.


title: Encapsulating Non-Determinacy in an Abstract Data Type with Determinate Semantics

abstract: Abstract A parallel program may be indeterminate so that it can adapt its behavior to the number of processors available. Indeterminate programs are hard to write, understand, modify or verify. They are impossible to debug, since they may not behave the same from one run to the next. We propose a new construct, a polymorphic abstract data type called an improving value , with operations that have indeterminate behavior but simple determinate semantics. These operations allow the type of indeterminate behavior required by many parallel algorithms. We define improving values in the context of a functional programming language, but the technique can be used in procedural programs as well.


title: A Semantic Basis for Quest

authors:
Luca Cardelli
Giuseppe Longo

abstract: Abstract Quest is a programming language based on impredicative type quantifiers and subtyping within a three-level structure of kinds, types and type operators, and values. The semantics of Quest is rather challenging. In particular, difficulties arise when we try to model simultaneously features such as contravariant function spaces, record types, subtyping, recursive types and fixpoints. In this paper we describe in detail the type inference rules for Quest, and give them meaning using a partial equivalence relation model of types. Subtyping is interpreted as in previous work by Bruce and Longo (1989), but the interpretation of some aspects – namely subsumption, power kinds, and record subtyping – is novel. The latter is based on a new encoding of record types. We concentrate on modelling quantifiers and subtyping; recursion is the subject of current work.


title: Modular Proof of Strong Normalization for the Calculus of Constructions

authors:
Herman Geuvers
Mark-Jan Nederhof

abstract: Abstract We present a modular proof of strong normalization for the Calculus of Constructions of Coquand and Huet (1985, 1988). This result was first proved by Coquand (1986), but our proof is more perspicious. The method consists of a little juggling with some systems in the cube of Barendregt (1989), which provides a fine structure of the calculus of constructions. It is proved that the strong normalization of the calculus of constructions is equivalent with the strong normalization of F ω. In order to give the proof, we first establish some properties of various type systems. Therefore, we present a general framework of typed lambda calculi, including many well-known ones.


title: A Partial Evaluator for the Untyped lambda-Calculus

authors:
Carsten K. Gomard
Neil D. Jones

abstract: Abstract This article describes theoretical and practical aspects of an implemented self-applicable partial evaluator for the untyped lambda-calculus with constants and a fixed point operator. To the best of our knowledge, it is the first partial evaluator that is simultaneously higher-order, non-trivial, and self-applicable. Partial evaluation produces a residual program from a source program and some of its input data. When given the remaining input data the residual program yields the same result that the source program would when given all its input data. Our partial evaluator produces a residual lambda-expression given a source lambda-expression and the values of some of its free variables. By self-application, the partial evaluator can be used to compile and to generate stand-alone compilers from a denotational or interpretive specification of a programming language. An essential component in our self-applicable partial evaluator is the use of explicit binding time information. We use this to annotate the source program, marking as residual the parts for which residual code is to be generated and marking as eliminable the parts that can be evaluated using only the data that is known during partial evaluation. We give a simple criterion, well-annotatedness, that can be used to check that the partial evaluator can handle the annotated higher-order programs without committing errors. Our partial evaluator is simple, is implemented in a side-effect free subset of Scheme, and has been used to compile and to generate compilers and a compiler generator. In this article we examine two machine-generated compilers and find that their structures are surprisingly natural.


title: Fixed Points and Frontiers: A New Perspective

authors:
Sebastian Hunt
Chris Hankin

abstract: Abstract Abstract interpretation is the collective name for a family of semantics-based techniques for compile-time analysis of programs. One of the most costly operations in automating such analyses is the computation of fixed points. The frontiers algorithm is an elegant method, invented by Chris Clack and Simon Peyton Jones, which addresses this issue. In this article we present a new approach to the frontiers algorithm based on the insight that frontiers represent upper and lower subsets of a function's argument domain. This insight leads to a new formulation of the frontiers algorithm for higher-order functions, which is considerably more concise than previous versions. We go on to argue that for many functions, especially in the higher-order case, finding fixed points is an intractable problem unless the sizes of the abstract domains are reduced. We show how the semantic machinery of abstract interpretation allows us to place upper and lower bounds on the values of fixed points in large lattices by working within smaller ones.


title: Domain Generating Functions for Solving Constraint Satisfaction Problems

authors:
François Major
Guy Lapalme
Robert Cedergren

abstract: Abstract This paper presents an application of functional programming: searching a domain for elements which satisfy certain constraints. We give a very general formulation of the problem and describe ‘generate and test’, ‘backtracking’ and ‘forward checking’ algorithms. We then introduce the concept of domain generating functions to capture a common optimization during the search process: using partial solutions to reduce the size of the search space. We compare the efficiency of the original algorithms and those using domain generating functions first with the ‘classical’ n -queens example, and then with a problem having larger domains to search which was inspired by an application in macromolecular structure determination. Using algorithms coded in Miranda, Haskell and Common Lisp, we show that a high order (lazy) functional language is a useful and efficient tool for prototyping search methods in large complex domains.


title: Equivalence in Functional Languages with Effects

authors:
Ian A. Mason
Carolyn L. Talcott

abstract: Abstract Traditionally the view has been that direct expression of control and store mechanisms and clear mathematical semantics are incompatible requirements. This paper shows that adding objects with memory to the call-by-value lambda calculus results in a language with a rich equational theory, satisfying many of the usual laws. Combined with other recent work, this provides evidence that expressive, mathematically clean programming languages are indeed possible.


title: Type Inference With Simple Subtypes

abstract: Abstract Subtyping appears in a variety of programming languages, in the form of the ‘automatic coercion’ of integers to reals, Pascal subranges, and subtypes arising from class hierarchies in languages with inheritance. A general framework based on untyped lambda calculus provides a simple semantic model of subtyping and is used to demonstrate that an extension of Curry's type inference rules are semantically complete. An algorithm G for computing the most general typing associated with any given expression, and a restricted, optimized algorithm GA using only atomic subtyping hypotheses are developed. Both algorithms may be extended to insert type conversion functions at compile time or allow polymorphic function declarations as in ML.


title: Using Transformations in the Implementations of Higher-Order Functions

authors:
Hanne Riis Nielson
Flemming Nielson

abstract: Abstract Traditional functional languages do not have an explicit distinction between binding times. It arises implicitly, however, as one typically instantiates a higher-order function with the arguments that are known, whereas the unknown arguments remain to be taken as parameters. The distinction between ‘ known ’ and ‘ unknown ’ is closely related to the distinction between binding times like ‘ compile-time ’ and ‘ run-time ’. This leads to the use of a combination of polymorphic type inference and binding time analysis for obtaining the required information about which arguments are known. Following the current trend in the implementation of functional languages we then transform the run-time level of the program (not the compile-time level) into categorical combinators . At this stage we have a natural distinction between two kinds of program transformations: partial evaluation , which involves the compile-time level of our notation, and algebraic transformations (i.e., the application of algebraic laws), which involves the run-time level of our notation. By reinterpreting the combinators in suitable ways we obtain specifications of abstract interpretations (or data flow analyses). In particular, the use of combinators makes it possible to use a general framework for specifying both forward and backward analyses . The results of these analyses will be used to enable program transformations that are not applicable under all circumstances. Finally, the combinators can also be reinterpreted to specify code generation for various (abstract) machines. To improve the efficiency of the code generated, one may apply abstract interpretations to collect extra information for guiding the code generation. Peephole optimizations may be used to improve the code at the lowest level.


title: Using Types as Search Keys in Function Libraries

abstract: Abstract A method is proposed to search for an identifier in a functional program library by using its Hindley–Milner type as a key. This can be seen as an approximation of using the specification as a key. Functions that only differ in their argument order or currying are essentially the same, which is expressed by a congruence relation on types. During a library search, congruent types are identified. If a programmer is not satisfied with the type of a found value, he can use a conversion function (like curry ), which must exist between congruent types, to convert the value into the type of his choice. Types are congruent if they are isomorphic in all cartesian closed categories. To put it more simply, types are congruent if they are equal under an arithmetical interpretation, with cartesian product as multiplication and function space as exponentiation. This congruence relation is characterized by seven equational axioms. There is a simple term-rewriting algorithm to decide congruence, using which a search system has been implemented for the functional language Lazy ML, with good performance. The congruence relation can also be used as a basis for other search strategies, e.g. searching for identifiers of a more general type, modulo congruence or allowing free type variables in queries.


title: Retrieving Reusable Software Components by Polymorphic Type

authors:
Colin Runciman
Ian Toyn

abstract: Abstract Polymorphic types are labels classifying both ( a ) defined components in a library and ( b ) contexts of free variables in partially written programs. It is proposed to help programmers make better use of software libraries by providing a system that, given ( b ), identifies candidates from ( a ) with matching types. Assuming at first that matching means unifying (i.e. having a common instance), efficient ways of implementing such a retrieval system are discussed and its likely effectiveness based on a quantitative study of currently available libraries is indicated. The applicative instance relation between types, which captures some intuitions about generalization/specialization is then introduced, and its use as the basis of a more flexible system is discussed.


title: A Run-Time Algorithm for Managing the Granularity of Parallel Functional Programs

authors:
Gad Aharoni
Dror G. Feitelson
Amnon Barak

abstract: Abstract We present an on-line (run-time) algorithm that manages the granularity of parallel functional programs. The algorithm exploits useful parallelism when it exists, and ignores ineffective parallelism in programs that produce many small tasks. The idea is to balance the amount of local work with the cost of distributing the work. This is achieved by ensuring that for every parallel task spawned, an amount of work that equals the cost of the spawn is performed locally. We analyse several cases and compare the algorithm to the optimal execution. In most cases the algorithm competes well with the optimal algorithm, even though the optimal algorithm has information about the future evolution of the computation that is not available to the on-line algorithm. This is quite remarkable considering we have chosen extreme cases that have contradicting optimal executions. Moreover, we show that no other on-line algorithm can be consistently better than it. We also present experimental results that demonstrate the effectiveness of the algorithm.


title: A Categorical Understanding of Environment Machines

abstract: Abstract In the last two decades, category theory has become one of the main tools for the denotational investigation of programming languages. Taking advantage of the algebraic nature of the categorical semantics, and of the rewriting systems it suggests, it is possible to use these denotational descriptions as a base for research into more operational aspects of programming languages. This approach proves to be particularly interesting in the study and the definition of environment machines for functional languages. The reason is that category theory offers a simple and uniform language for handling terms and environments (substitutions), and for studying their interaction (through application). Several examples of known machines are discussed, among which the Categorical Abstract Machine of Cousineau et al. (1987) and Krivine's machine. Moreover, as an example of the power and fruitfulness of this approach, we define two original categorical machines. The first one is a variant of the CAM implementing a λ-calculus with both call-by-value and call-by-name as parameters passing modes. The second one is a variant of Krivine's machine performing complete reduction of λ-terms.


title: Enumerators of lambda Terms are Reducing

abstract: Abstract A closed λ-term E is called an enumerator if Here ⋀ 0 is the set of closed λ-terms,. is the set of natural numbers and the ⌜ n ⌝ are the Church's numerals λ fx . f n x . Such an E is called reducing if, moreover An ingenious recursion theoretic proof by Statman will be presented, showing that every enumerator is reducing. I do not know any direct proof.


title: Representing 'undefined' in lambda Calculus

abstract: Abstract Let ψ be a partial recursive function (of one argument) with λ-defining term F ∈Λ°. This means There are several proposals for what F ⌜ n ⌝ should be in case ψ( n ) is undefined: (1) a term without a normal form (Church); (2) an unsolvable term (Barendregt); (3) an easy term (Visser); (4) a term of order 0 (Statman). These four possibilities will be covered by one ‘master’ result of Statman which is based on the ‘Anti Diagonal Normalization Theorem’ of Visser (1980). That ingenious theorem about precomplete numerations of Ershov is a powerful tool with applications in recursion theory, metamathematics of arithmetic and lambda calculus.


title: Two Greedy Algorithms

abstract: At the recent TC2 working conference on constructing programs from specifications (Moeller, 1991), I presented the derivation of a functional program for solving a problem posed by Knuth (1990). Slightly simplified, the problem was to construct a shortest decimal fraction representing a given integer multiple of 1/2 16 . Later in the conference – and in a different context – Robert Dewar described a second problem that he had recently set as an examination question. In brief, the problem was to replace sequences of blanks in a file by tab characters wherever possible. Although Knuth's and Dewar's problems appear to have little in common, I suspected that both had the same ‘deep structure’ and were instances of a single general result about greedy algorithms. The purpose of this note is to bring the genral result to light and to unify the treatment of the two problems. We begin by describing the problems more precisely.


title: Unravelling Greedy Algorithms

abstract: In my previous Functional Pearls article (Bird, 1992), I proved a theorem giving conditions under which an optimization problem could be implemented by a greedy algorithm. A greedy algorithm is one that picks a ‘best’ element at each stage. Here, we return to this theorem and extend it in various ways. We then use the theory to solve an intriguing problem about unravelling sequences into a smallest number of ascending subsequences.


title: Abstract Interpretation by Dynamic Partitioning

abstract: Abstract The essential part of abstract interpretation is to build a machine-representable abstract domain expressing interesting properties about the possible states reached by a program at runtime. Many techniques have been developed which assume that one knows in advance the class of properties that are of interest. There are cases however when there are no a priori indications about the 'best' abstract properties to use. We introduce a new framework that enables non-unique representations of abstract program properties to be used, and expose a method, called dynamic partitioning, that allows the dynamic determination of interesting abstract domains using data structures built over simpler domains. Finally, we show how dynamic partitioning can be used to compute non-trivial approximations of functions over infinite domains and give an application to the computation of minimal function graphs.


title: A Practical Functional Program for the CRAY X-MP

authors:
James M. Boyle
Terence J. Harmer

abstract: Abstract One can have all the advantages of functional programming – correctness, clarity, simplicity, and flexibility – without any sacrifice in performance, even for a scientifically significant computation on a supercomputer. Therefore, why use Fortran? We demonstrate parity – equality of speed and storage use – between a program generated automatically from a functional specification and a program written by hand in the procedural style. To our knowledge, this demonstration of parity is the first for a program that solves a scientifically significant problem – quasi-linear hyperbolic partial differential equations – on a scientifically interesting supercomputer – the CRAY X-MP. We use pure Lisp, including higher-order functions, to express the functional specification for the PDE solver. We designed this specification for maximal clarity and flexibility, rather than for efficiency. Nevertheless, we obtain a highly efficient program to solve the PDEs: automated program transformations put back the missing efficiency as they produce an executable Fortran program from the specification. The generated Fortran program vectorizes on the CRAY X-MP and runs about 4% faster than a handwritten Fortran program for the same problem. We describe the problem and the specification, and some of the problem-domain-specific and hardware-specific transformations that we use to obtain the high-efficiency program.


title: Modelling Operating System Structures by Timed Stream Processing Functions

authors:
Manfred Broy
Claus Dendorfer

abstract: Abstract Some extensions of the basic formalism of stream processing functions are useful to specify complex structures such as operating systems. In this paper we give the foundations of higher order stream processing functions. These are functions which send and accept not only messages representing atomic data, but also complex elements such as functions. Some special notations are introduced for the specification and manipulation of such functions. A representation of time is outlined, which enables us to model time dependent behaviour. Finally, we demonstrate how characteristic operating system structures can be modelled by timed higher order stream processing functions.


title: MetaMorph - A Formal Methods Toolkit with Application to the Design of Digital Hardware

abstract: Abstract MetaMorph is a software tool that supports transformation and proof for an equational non-strict functional language. It was developed as a vehicle for research into the synthesis of digital logic, but is equally suitable for reasoning about functional programs. The theorem prover may be used for verifying new reusable transforms and to assist the search for transformation sequences having a constrained goal. The paper provides an overview of all aspects of the project, and a brief discussion of its application to hardware.


title: Distributed Random Number Generation

authors:
F. Warren Burton
Rex L. Page

abstract: Abstract In a functional program, a simple random number generator may generate a lazy list of random numbers. This is fine when the random numbers are consumed sequentially at a single point in the program. However, things are more complicated in a program where random numbers are used at many locations, such as in a large simulation. The programmer should not need to worry about providing separate generators with a unique seed at each point where random numbers are used. At the same time, the programmer should not need to coordinate the use of a single stream of random numbers in many parts of the program, which can be particularly difficult with lazy evaluation or parallel processing. We discuss several techniques for distributing random numbers to various parts of a program, and some methods of allowing different program components to evaluate random numbers locally. We then propose a new approach in which a random number sequence can be split at a random point to produce a pair of random number sequences that can be used independently at different points in the computation. The approach can also be used in distributed procedural programs, where it is desirable to avoid dealing with a single source of random numbers. The approach has the added advantage of producing repeatable results, as might be needed in debugging, for example.


title: A Symmetric Set of Efficient List Operations

abstract: In this paper we show that it is possible to implement a symmetric set of finite-list operations efficiently; the set is symmetric in the sense that lists can be manipulated at either end. We derive the definitions of these operations from their specifications by calculation. The operations have O(1) time complexity, provided that we content ourselves with, so-called, amortized efficiency , instead of worst-case efficiency


title: Higher-Order Functions for Parsing

abstract: Abstract In combinator parsing , the text of parsers resembles BNF notation. We present the basic method, and a number of extensions. We address the special problems presented by white-space, and parsers with separate lexical and syntactic phases. In particular, a combining form for handling the ‘offside rule’ is given. Other extensions to the basic method include an ‘into’ combining form with many useful applications, and a simple means by which combinator parsers can produce more informative error messages.


title: Tail Recursion without Space Leaks

abstract: Abstract The G-machine (Johnsson, 1987; Peyton Jones, 1987) is a compiled graph reduction machine for lazy functional languages. The G-machine compiler contains many optimizations to improve performance. One set of such optimizations is designed to improve the performance of tail recursive functions. Unfortunately, the abstract machine is subject to a space leak—objects are unnecessarily preserved by the garbage collector. This paper analyses why a particular form of space leak occurs in the G-machine, and presents some ideas for fixing this problem. This phenomena in other abstract machines is also examined briefly.


title: Implementing Lazy Functional Languages on Stock Hardware: The Spineless Tagless G-Machine

abstract: Abstract The Spineless Tagless G-machine is an abstract machine designed to support non-strict higher-order functional languages. This presentation of the machine falls into three parts. Firstly, we give a general discussion of the design issues involved in implementing non-strict functional languages. Next, we present the STG language , an austere but recognizably-functional language, which as well as a denotational meaning has a well-defined operational semantics. The STG language is the ‘abstract machine code’ for the Spineless Tagless G-machine. Lastly, we discuss the mapping of the STG language onto stock hardware. The success of an abstract machine model depends largely on how efficient this mapping can be made, though this topic is often relegated to a short section. Instead, we give a detailed discussion of the design issues and the choices we have made. Our principal target is the C language, treating the C compiler as a portable assembler.


title: Computing with Lattices: An Application of Type Classes

abstract: Abstract This paper presents a simple framework for performing calculations with the elements of (finite) lattices. A particular feature of this work is the use of type classes to enable the use of overloaded function symbols within a strongly typed language. Previous applications of type classes have been in areas that are of most interest to language implementors. This paper suggests that type classes might also be useful as a general tool in the development of clear and modular programs.


title: Quantifier Elimination and Parametric Polymorphism in Programming Languages

abstract: Abstract We present a simple and easy-to-understand explanation of ML type inference and parametric polymorphism within the framework of type monomorphism, as in the first order typed lambda calculus. We prove the equivalence of this system with the standard interpretation using type polymorphism, and extend the equivalence to include polymorphic fixpoints. The monomorphic interpretation gives a purely combinatorial understanding of the type inference problem, and is a classic instance of quantifier elimination, as well as an example of Gentzen-style cut elimination in the framework of the Curry-Howard propositions-as-types analogy.


title: Efficient Self-Interpretations in lambda Calculus

abstract: Abstract We start by giving a compact representation schema for λ-terms, and show how this leads to an exceedingly small and elegant self-interpreter. We then define the notion of a self-reducer , and show how this too can be written as a small λ-term. Both the self-interpreter and the self-reducer are proved correct. We finally give a constructive proof for the second fixed point theorem for the representation schema. All the constructions have been implemented on a computer, and experiments verify their correctness. Timings show that the self-interpreter and self-reducer are quite efficient, being about 35 and 50 times slower than direct execution using a call-by-need reductions strategy


title: A Domain-Theoretic Approach to Functional and Logic Programming

authors:
Frank S. K. Silbermann
Bharat Jayaraman

abstract: Abstract The integration of functional and logic programming languages has been a topic of great interest in the last decade. Many proposals have been made, yet none is completely satisfactory especially in the context of higher order functions and lazy evaluation. This paper addresses these shortcomings via a new approach: domain theory as a common basis for functional and logic programming. Our integrated language remains essentially within the functional paradigm. The logic programming capability is provided by set abstraction (via Zermelo-Frankel set notation), using the Herbrand universe as a set abstraction generator, but for efficiency reasons our proposed evaluation procedure treats this generator's enumeration parameter as a logical variable. The language is defined in terms of (computable) domain-theoretic constructions and primitives, using the lower (or angelic) powerdomain to model the set abstraction facility. The result is a simple, elegant and purely declarative language that successfully combines the most important features of both pure functional programming and pure Horn logic programming. Referential transparency with respect to the underlying mathematical model is maintained throughout. An implicitly correct operational semantics is obtained by direct execution of the denotational semantic definition, modified suitably to permit logical variables whenever the Herbrand universe is being generated within a set abstraction. Completeness of the operational semantics requires a form of parallel evaluation, rather than the more familiar left-most rule.


title: Polymorphic Type, Region and Effect Inference

authors:
Jean-Pierre Talpin
Pierre Jouvelot

abstract: Abstract We present a new static system which reconstructs the types, regions and effects of expressions in an implicitly typed functional language that supports imperative operations on reference values. Just as types structurally abstract collections of concrete values, regions represent sets of possibly aliased reference values and effects represent approximations of the imperative behaviour on regions. We introduce a static semantics for inferring types, regions and effects, and prove that it is consistent with respect to the dynamic semantics of the language. We present a reconstruction algorithm that computes the types and effects of expressions, and assigns regions to reference values. We prove the correctness of the reconstruction algorithm with respect to the static semantics. Finally, we discuss potential applications of our system to automatic stack allocation and parallel code generation.


title: A Study of Sparse Matrix Representations for Solving Linear Systems in a Functional Language

authors:
Roger L. Wainwright
Marian E. Sexton

abstract: Abstract This paper compares three different sparse matrix representations in Miranda for solving linear systems of equations: quadtrees, binary trees and run-length encoding. It compares the three data structures in each of two common linear system solvers, Conjugate Gradient and SOR. The test problems used in the paper arise from a simple reservoir model.


title: Efficient Sets - A Balancing Act

abstract: Capsule ReviewIn late 1991 I organized an international programming competition for the Standard ML community.Each entrant implemented the 'set of integers' abstract data type, matching a signature that I provided.Prizes (donated by MIT Press) were awarded in two categories: fastest program (on a particular benchmark), and most elegant yet still efficient program.More than a dozen entries were received; the top four entries in the speed category are listed here:1


title: A Critique of Standard ML

abstract: Abstract Standard ML is an excellent language for many kinds of programming. It is safe, efficient, suitably abstract, and concise. There are many aspects of the language that work well. However, nothing is perfect: Standard ML has a few shortcomings. In some cases there are obvious solutions, and in other cases further research is required.


title: The Interactive Lazy ML System

abstract: Abstract In this paper we describe an implementation of an interactive version of the purely functional programming language Lazy ML (LML). The most remarkable fact about the interactive system is that it is written in a pure functional style using LML, yet the efficiency still compares favourably to other conventional interpretative systems. We describe how the system is designed, and also the exception mechanism that was added to facilitate the handling of errors in the system.