Package managers are legion. Every programming language and operating system has its own solution, each with subtly different semantics for dependency resolution. This fragmentation prevents multilingual projects from expressing precise dependencies across language ecosystems; it leaves external system dependencies implicit and unversioned; and it obscures the full dependency graph that supply-chain analysis depends on. We present the Package Calculus, a formalism for dependency resolution that unifies the core semantics of package managers. Through a series of formal reductions, we show how this core is expressive enough to model the diversity of real-world dependency expression languages. The calculus provides the theoretical foundation for future cross-ecosystem tooling, as a lingua franca of dependency expression.

Efficient on-device neural network (NN) inference offers predictable latency, improved privacy and reliability, and lower operating costs for vendors than cloud-based inference. This has sparked recent development of microcontroller-scale NN accelerators, also known as neural processing units (μNPUs), designed specifically for ultra-low-power applications.

Docker is a developer tool used by millions of developers to build, share and run software stacks. The Docker Desktop clients for Mac and Windows have long used a novel combination of virtualisation and OCaml unikernels to seamlessly run Linux containers on these non-Linux hosts. We reflect on a decade of shipping this functional OCaml code into production across hundreds of millions of developer desktops, and discuss the lessons learnt from our experiences in integrating OCaml deeply into the container architecture that now drives much of the global cloud. We conclude by observing just how good a fit for systems programming that the unikernel approach has been, particularly when combined with the OCaml module and type system.

Modern datacenters run diverse workloads that increasingly comprise data-parallel computational jobs. There has been a steady rise in their demand leading to high-volume traffic. To meet these demands, datacenter providers operate their clusters at levels of high utilization. We show that under such conditions, existing schedulers impose large wait times on tail tasks, leading to long job completion time. We propose a new decentralized scheduler, Murmuration, that reduces the total wait time of tasks. It employs multiple communicating schedulers to schedule tasks of jobs such that their start times are as close together as possible, ensuring small tail task completion time and better average job completion time.

Carbon credits purchased in the voluntary carbon market allow unavoidable emissions, such as international flights for essential travel, to be offset by an equivalent climate benefit, such as avoiding emissions from tropical deforestation. However, many concerns regarding the credibility of these offsetting claims have been raised. Moreover, the credit market is manual, therefore inefficient and unscalable, and non-fungible, therefore illiquid. To address these issues, we propose an efficient digital methodology that combines remote sensing data, modern econometric techniques, and on-chain certification and trading to create a new digital carbon asset (the PACT stablecoin) against which carbon offsetting claims can be transparently verified. PACT stablecoins are produced as outputs from a reproducible computational pipeline for estimating the climate benefits of carbon offset projects that not only quantifies the CO2 emissions involved, but also allows for similar credits to be pooled based on their co-benefits such as biodiversity and jurisdictional attributes, increasing liquidity through fungibility within pools. We implement and evaluate the PACT carbon stablecoin on the Tezos blockchain, which is designed to facilitate low-cost transactions while minimizing environmental impact. Our implementation includes a contract for a registry for tracking issuance, ownership, and retirement of credits, and a custodian contract to bridge on-chain and off-chain transactions. Our work brings scale and trust to the voluntary carbon market by providing a transparent, scalable, and efficient framework for high-integrity carbon credit transactions.

The Kunming-Montreal Global Biodiversity Framework sets ambitious targets for 2023, including halting human-induced species extinction. Achieving these requires comprehensive data on global biodiversity patterns, which can only be gathered through in-situ distributed sensor networks. However, these multi-device networks are constrained by battery lifetimes, must gather rich data from power-hungry sensors, and yet need to be deployed in remote environments for long periods. This note introduces a prototype multi-sensor device, and outlines how embedded scheduling could be used for extending sensor lifetime and resource-efficiency.

The existing Internet architecture lacks support for naming locations and resolving them to the myriad addressing mechanisms we use beyond IP. We propose the Spatial Name System (SNS) that allows for the assignment of hierarchical location-based names and for resolution schemes that are both global and local. Since we extend the DNS, our scheme allows for the integration of spatial names into existing applications and opens up new possibilities for sensor networks and augmented reality.

We are now seeing increased hardware support for improving the security and performance of privilege separation and compartmentalization techniques. Today, developers can benefit from multiple compartmentalization mechanisms such as process-based sandboxes, trusted execution environments (TEEs)/enclaves, and even intra-address space compartments (i.e., intra-process or intra-enclave). We dub such a computing model a “hetero-compartment” environment and observe that existing system stacks still assume single-compartment models (i.e., user space processes), leading to limitations in using, integrating, and monitoring heterogeneous compartments from a security and performance perspective.

Effect handlers have been gathering momentum as a mechanism for modular programming with user-defined effects. Effect handlers allow for non-local control flow mechanisms such as generators, async/await, lightweight threads and coroutines to be composably expressed. We present a design and evaluate a full-fledged efficient implementation of effect handlers for OCaml, an industrial-strength multi-paradigm programming language. Our implementation strives to maintain the backwards compatibility and performance profile of existing OCaml code. Retrofitting effect handlers onto OCaml is challenging since OCaml does not currently have any non-local control flow mechanisms other than exceptions. Our implementation of effect handlers for OCaml: (i) imposes a mean 1% overhead on a comprehensive macro benchmark suite that does not use effect handlers; (ii) remains compatible with program analysis tools that inspect the stack; and (iii) is efficient for new code that makes use of effect handlers.

OCaml is an industrial-strength, multi-paradigm programming language, widely used in industry and academia. OCaml is also one of the few modern managed system programming languages to lack support for shared memory parallel programming. This paper describes the design, a full-fledged implementation and evaluation of a mostly-concurrent garbage collector (GC) for the multicore extension of the OCaml programming language. Given that we propose to add parallelism to a widely used programming language with millions of lines of existing code, we face the challenge of maintaining backwards compatibility--not just in terms of the language features but also the performance of single-threaded code running with the new GC. To this end, the paper presents a series of novel techniques and demonstrates that the new GC strikes a balance between performance and feature backwards compatibility for sequential programs and scales admirably on modern multicore processors.

We propose a new semantics for shared-memory parallel programs that gives strong guarantees even in the presence of data races. Our local data race freedom property guarantees that all data-race-free portions of programs exhibit sequential semantics. We provide a straightforward operational semantics and an equivalent axiomatic model, and evaluate an implementation for the OCaml programming language. Our evaluation demonstrates that it is possible to balance a comprehensible memory model with a reasonable (no overhead on x86, ~0.6% on ARM) sequential performance trade-off in a mainstream programming language.

Systems depend critically on the behaviour of file systems, but that behaviour differs in many details, both between implementations and between each implementation and the POSIX (and other) prose specifications. Building robust and portable software requires understanding these details and differences, but there is currently no good way to systematically describe, investigate, or test file system behaviour across this complex multi-platform interface.

The Commercial Users of Functional Programming workshop (CUFP) is an annual workshop held in association with the International Conference on Functional Programming (ICFP). The aim of the CUFP workshops is to publicize the use of functional programming in commercial ventures. Its motto is “functional programming as a means, not an end.

We present unikernels, a new approach to deploying cloud services via applications written in high-level source code. Unikernels are single-purpose appliances that are compile-time specialised into standalone kernels, and sealed against modification when deployed to a cloud platform. In return they offer significant reduction in image sizes, improved efficiency and security, and should reduce operational costs. Our Mirage prototype compiles OCaml code into unikernels that run on commodity clouds and offer an order of magnitude reduction in code size without significant performance penalty. The architecture combines static type-safety with a single address-space layout that can be made immutable via a hypervisor extension. Mirage contributes a suite of type-safe protocol libraries, and our results demonstrate that the hypervisor is a platform that overcomes the hardware compatibility issues that have made past library operating systems impractical to deploy in the real-world.

Datacenter networking has brought high-performance storage systems' research to the foreground once again. Many modern storage systems are built with commodity hardware and TCP/IP networking to save costs. In this paper, we highlight a group of problems that are present in such storage systems and which are all related to the use of TCP. As an alternative, we explore Trevi: a fountain coding-based approach for distributing I/O requests that overcomes these problems while still efficiently scheduling resources across both networking and storage layers. We also discuss how receiver-driven flow and congestion control, in combination with fountain coding, can guide the design of Trevi and provide a viable alternative to TCP for datacenter storage.

Commercial Users of Functional Programming (CUFP) is an annual workshop that is aimed at the community of software developers who use functional programming in real-world settings. This scribe report covers the talks that were delivered at the 2012 workshop, which was held in association with International Conference on Functional Programming (ICFP) in Copenhagen, Denmark. The goal of the report is to give the reader a sense of what went on, rather than to reproduce the full details of the talks. Videos and slides from all the talks are available online at http://cufp.org.

OS virtualization and cloud computing have radically changed the way Internet services are deployed: enterprises share third-party datacenters, deploying existing applications with minimal changes. Recent measurements reveal a lack of traffic isolation capabilities within the datacenter with network performance exhibiting high variability. We advocate addressing this problem by allowing applications to express their own forwarding logic using OpenFlow to achieve application specific optimal performance. We present an OpenFlow implementation within the Mirage application synthesis framework, in the form of library implementations of a modular controller and an extensible OpenFlow-enabled switch, able to expose the underlying network infrastructure to cloud applications. By linking into the application, this provides a safe yet highly extensible framework for programming network control that, although unoptimised, still provides reasonable performance when compared with existing controllers.

This demo presents Signposts, a system to provide users with a secure, simple mechanism to establish and maintain communication channels between their personal cloud of named devices. Signpost names exist in the DNSSEC hierarchy, and resolve to secure end-points when accessed by existing DNS clients. Signpost clients intercept user connection intentions while adding privacy and multipath support. Signpost servers co-ordinate clients to dynamically discover routes and overcome the middleboxes that pervade modern edge networks. The demo will show a simple scenario where an individual's personal devices (phone, laptop) are interconnected via Signposts while sitting on different networks behind various middleboxes. As a result they will be able to fetch and push data between each other, demonstrated by, e.g., simple web browsing, even as the network configuration changes.

Commercial Users of Functional Programming (CUFP) is a yearly workshop that is aimed at the community of software developers who use functional programming in real-world settings. This scribe report covers the talks that were delivered at the 2011 workshop, which was held in association with ICFP in Tokyo. The goal of the report is to give the reader a sense of what went on, rather than to reproduce the full details of the talks. Videos and slides from all the talks are available online at http://cufp.org .

Reconfigurable computing in the cloud helps to solve many practical problems relating to scaling out data-centers where computation is limited by energy consumption or latency. However, for reconfigurable computing in the cloud to become practical several research challenges have to be addressed. This paper identifies some of the perquisites for reconfigurable computing systems in the cloud and picks out several scenarios made possible with immense cloud-based computing capability.

We present a case-study of using OCaml within a large product development project, focussing on both the technical and non-technical issues that arose as a result. We draw comparisons between the OCaml team and the other teams that worked on the project, providing comparative data on hiring patterns and cross-team code contribution.

This paper presents an architecture that affords mobile users greater trust and security when browsing the internet (e.g., when making personal/financial transactions) from public terminals at Internet Cafes or other unfamiliar locations. This is achieved by enabling web applications to split their client-side pages across a pair of browsers: one untrusted browser running on a public PC and one trusted browser running on the user's personal mobile device, composed into a single logical interface through a local connection, wired or wireless. Information entered via the personal device's keypad cannot be read by the PC, thwarting PC-based key-loggers. Similarly, information displayed on the personal device's screen is also hidden from the PC, preserving the confidentiality and integrity of security-critical data even in the presence of screen grabbing attacks and compromised PC browsers. We present a security policy model for split-trust web applications that defends against a range of crimeware-based attacks, including those based on active-injection (e.g. inserting malicious packets into the network or spoofing user-input events). Performance results of a prototype split-trust implementation are presented, using a commercially available cell phone as a trusted personal device.

Most implementations of critical Internet protocols are written in type-unsafe languages such as C or C++ and are regularly vulnerable to serious security and reliability problems. Type-safe languages eliminate many errors but are not used to due to the perceived performance overheads.