OxCaml extends the OCaml type system with support for safe low-level systems programming via modes . For example, OxCaml’s modal portability and contention axes ensure that concurrent OxCaml programs have no data races. In practice, however, modal tracking can reject programs that are obviously safe, such as when the data shared across threads is immutable. To remedy this problem, we introduce mode crossing —the ability to automatically strengthen modes ( e.g. , from nonportable to portable) for values of certain types. Mode crossing significantly reduces the annotation burden associated with modal types. To support mode crossing in the presence of abstract type specifications, we further introduce a new type system feature, modal kinds . We present a type-theoretic account of modal kinds, interpret them as monotone functions on a lattice of modes, and extend this interpretation to recursive and abstract types. We verify soundness of the modal kind system in Rocq on top of Iris. We design an inference procedure that reduces kind checking and subsumption to constraints solved by a dedicated lattice solver. Our design is implemented in the OxCaml compiler and deployed in a large industrial codebase, demonstrating practical usability.

The initial TCP slow start phase seeks to ramp up data transmission rates quickly to meet available capacity but also to exit the slow start phase before causing undue congestion. Unfortunately, the typical default TCP implementation often exits slow start too early, before capacity has been reached, causing underutilization, particularly detrimental to networks with large capacities and high delays. This study introduces a novel enhancement to TCP slow start - Slow start Exit At Right CHokepoint (SEARCH) - where the link capacity is inferred at the server based on bytes delivered compared to the expected bytes delivered, smoothed to account for link latency variation and normalized to accommodate link capacities. Empirical evaluation over geosynchronous satellite links, low-orbit satellite links, and 4G LTE links shows our approach is a substantial improvement over default TCP implementations by not exiting slow start too early, but better than traditional TCP, too, by exiting slow start before encountering packet loss.

The Slow start Exit At Right CHokepoint (SEARCH) algorithm is designed to exit the TCP slow start phase after the flow has reached the link capacity but before packets have been lost. To do this, SEARCH keeps a history of the bytes delivered over a recent time window, aggregated into bins. Unfortunately, this delivery history must be kept per-flow, adding additional memory load for each TCP connection. We address this per-flow memory load by observing that SEARCH only needs the relative number of bytes delivered and propose a bit-shifting technique that dynamically compresses bin values as needed. Our approach is tunable to the memory-use reduction required compared to the delivery precision needed. Evaluation of our approach over a satellite network shows SEARCH bin memory use can be reduced by 50% or even 75% without any significant sacrifice in SEARCH algorithm accuracy. Our approach is generalizable to other network algorithms, too, reducing memory use for algorithms that use sliding windows and historical data tracking.

TCP’s slow start phase is particularly inefficient over most wireless networks, especially high-latency, high-bandwidth paths such as satellite networks, often exiting too early or too late (after packet loss). To address this, the Slow start Exit At CHokepoint (SEARCH) algorithm is designed to improve exit decisions during slow start by analyzing delivery trends across sliding RTT-based windows. This paper presents a first implementation of SEARCH in the FreeBSD kernel using FreeBSD’s modular congestion control framework. We evaluate our implementation on a testbed with an actual GEO satellite link with ~600 ms RTT and 150 Mb/s capacity. Preliminary results show that SEARCH exits slow start more effectively than HyStart and HyStart++, achieving higher throughput and better utilization.

We present DRFCaml, an extension of OCaml’s type system that guarantees data race freedom for multithreaded OCaml programs while retaining backward compatibility with existing sequential OCaml code. We build on recent work of Lorenzen et al., who extend OCaml with modes that keep track of locality, uniqueness, and affinity. We introduce two new mode axes, contention and portability , which record whether data has been shared or can be shared between multiple threads. Although this basic type-and-mode system has limited expressive power by itself, it does let us express APIs for capsules , regions of memory whose access is controlled by a unique ghost key, and reader-writer locks , which allow a thread to safely acquire partial or full ownership of a key. We show that this allows complex data structures (which may involve aliasing and mutable state) to be safely shared between threads. We formalize the complete system and establish its soundness by building a semantic model of it in the Iris program logic on top of the Rocq proof assistant.

QUIC is increasingly being deployed on the Internet as an alternative to TCP. However, QUIC over satellite links faces particular challenges as high and variable round-trip times (RTTs) make it difficult to determine and then reach link capacity. Standard slow start algorithms to detect link capacity can perform poorly over satellite links, often exiting slow start too early and limiting throughput or exiting too late and causing unnecessary packet loss. The Slow start Exit At Right CHokepoint (SEARCH) algorithm aims to exit slow start after reaching link capacity but before incurring packet loss by tracking delivery rates and exiting when rates have not increased by the expected amount. SEARCH has shown benefits over traditional slow start for TCP connections but has yet to be implemented and evaluated in QUIC. This paper presents the design and implementation of SEARCH in an open-source QUIC library, with the code publicly available as a contribution. Evaluation of SEARCH over a geostationary satellite link show SEARCH successfully exits slow start before loss in the majority of cases, Improving goodput compared to the baseline.

Gödel published his groundbreaking first incompleteness theorem in 1931, stating that a large class of formal logics admits independent sentences which are neither provable nor refutable. This result, in conjunction with his second incompleteness theorem, established the impossibility of concluding Hilbert’s program, which pursued a possible path towards a single formal system unifying all of mathematics. Using a technical trick to refine Gödel’s original proof, the incompleteness result was strengthened further by Rosser in 1936 regarding the conditions imposed on the formal systems. Computability theory, which also originated in the 1930s, was quickly applied to formal logics by Turing, Kleene, and others to yield incompleteness results similar in strength to Gödel’s original theorem, but weaker than Rosser’s refinement. Only much later, Kleene found an improved but far less well-known proof based on computational notions, yielding a result as strong as Rosser’s. In this expository paper, we work in constructive type theory to reformulate Kleene’s incompleteness results abstractly in the setting of synthetic computability theory and assuming a form of Church’s thesis, an axiom internalising the fact that all functions definable in such a setting are computable. Our novel, greatly condensed reformulation showcases the simplicity of the computational argument while staying formally entirely precise, a combination hard to achieve in typical textbook presentations. As an application, we instantiate the abstract result to first-order logic in order to derive essential incompleteness and, along the way, essential undecidability of Robinson arithmetic. This paper is accompanied by a Coq mechanisation covering all our results and based on existing libraries of undecidability proofs and first-order logic, complementing the extensive work on mechanised incompleteness using the Gödel-Rosser approach. In contrast to the related mechanisations, our development follows Kleene’s ideas and utilises Church’s thesis for additional simplicity.

TCP slow start begins at a conservative bitrate but quickly ramps up to the available bandwidth. Unfortunately, current TCP implementations can either: 1) exit from slow start prematurely, which is especially detrimental to utilization on satellite links, or 2) exit from slow start too late, causing unnecessary packet loss. We propose a novel technique to exit slow start while avoiding both premature and belated exits. We evaluate our approach over commercial satellite links - long, fat networks that pose challenges to determining the right slow start exit time. Preliminary results show a high success rate for picking appropriate exit points over satellite links, with potentially being applicable to other types of networks, more generally.

Understanding how new TCP congestion control algorithms interact with the default TCP Cubic over a wide-range of network conditions is important for moving congestion control research forward. Unfortunately, lacking are studies over actual satellite Internet networks where high latencies pose challenges to TCP performance. This paper presents results from experiments over a commercial satellite Internet link assessing TCP congestion control algorithm performance for Cubic when competing with algorithms using four different approaches: loss-based (Cubic), bandwidth-estimation based (BBR), utility function-based (PCC) and satellite optimized (Hybla). Analysis shows: 1) the default Cubic algorithms are fair to each other; 2) Cubic dominates PCC during steady state; 3) Hybla dominates Cubic during start-up; and 4) BBR dominates Cubic during both start-up and steady state.