
CommunityNews
A Flexible Type System for Fearless Concurrency
Abstract
This paper proposes a new type system for concurrent pro- grams, allowing threads to exchange complex object graphs without risking destructive data races. While this goal is shared by a rich history of past work, existing solutions ei- ther rely on strictly enforced heap invariants that prohibit natural programming patterns or demand pervasive annota- tions even for simple programming tasks. As a result, past systems cannot express intuitively simple code without un- natural rewrites or substantial annotation burdens. Our work avoids these pitfalls through a novel type system that pro- vides sound reasoning about separation in the heap while remaining flexible enough to support a wide range of desir- able heap manipulations. This new sweet spot is attained by enforcing a heap domination invariant similarly to prior work, but tempering it by allowing complex exceptions that add little annotation burden. Our results include: (1) code examples showing that common data structure manipula- tions which are difficult or impossible to express in prior work are natural and direct in our system, (2) a formal proof of correctness demonstrating that well-typed programs can- not encounter destructive data races at run time, and (3) an efficient type checker implemented in Gallina and OCaml.
Read in full here:
https://www.cs.cornell.edu/andru/papers/gallifrey-types/
This thread was posted by one of our members via one of our news source trackers.
Popular General Dev topics










Other popular topics










Latest in General Dev
Latest (all)
Categories:
Popular Portals
- /elixir
- /rust
- /wasm
- /ruby
- /erlang
- /phoenix
- /keyboards
- /js
- /rails
- /python
- /security
- /go
- /swift
- /vim
- /clojure
- /java
- /haskell
- /emacs
- /svelte
- /onivim
- /typescript
- /crystal
- /c-plus-plus
- /tailwind
- /kotlin
- /gleam
- /react
- /flutter
- /elm
- /ocaml
- /vscode
- /opensuse
- /centos
- /ash
- /php
- /deepseek
- /zig
- /scala
- /html
- /debian
- /nixos
- /lisp
- /agda
- /sublime-text
- /textmate
- /react-native
- /kubuntu
- /arch-linux
- /revery
- /ubuntu
- /manjaro
- /django
- /spring
- /diversity
- /nodejs
- /lua
- /julia
- /c
- /slackware
- /neovim