CommunityNews

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.

Where Next?

Popular Backend topics Top

First poster: AstonJ
Wren is a small, fast, class-based concurrent scripting language. Think Smalltalk in a Lua-sized package with a dash of Erlang and wrapp...
New
CommunityNews
Microsoft is trying to leapfrog competitors like Google and Amazon as they face record antitrust scrutiny. The big picture: The deals ...
New
First poster: bot
C++ Programming - The State of Developer Ecosystem in 2021 Infographic. The State of Developer Ecosystem 2021 is a detailed report about...
New
CommunityNews
Where does all the effort go? Looking at Python core developer activity - Łukasz Langa. One of the tasks given me by the Python Software...
New
CommunityNews
By the end of this guide we’ll have a minimal, working implementation of a small part of Lua from scratch.
New
First poster: mafinar
8 Reasons why Clojure is a better Java than Java. Clojure is better than Java at its own game. Using code examples, we dive into what ma...
New
First poster: bot
clog/LEARN.md at main · rabbibotton/clog. CLOG - The Common Lisp Omnificent GUI. Contribute to rabbibotton/clog development by creating ...
New
First poster: bot
GitHub - tetratelabs/wazero: wazero: the zero dependency WebAssembly runtime for Go developers. wazero: the zero dependency WebAssembly ...
New
First poster: bot
GitHub - codic12/worm: A dynamic, tag-based window manager written in Nim. A dynamic, tag-based window manager written in Nim - GitHub -...
New
First poster: bot
crubit/design.md at main · google/crubit. Contribute to google/crubit development by creating an account on GitHub.
New

Other popular topics Top

malloryerik
Any thoughts on Svelte? Svelte is a radical new approach to building user interfaces. Whereas traditional frameworks like React and Vue...
New
siddhant3030
I’m thinking of buying a monitor that I can rotate to use as a vertical monitor? Also, I want to know if someone is using it for program...
New
dasdom
No chair. I have a standing desk. This post was split into a dedicated thread from our thread about chairs :slight_smile:
New
Rainer
Not sure if following fits exactly this thread, or if we should have a hobby thread… For many years I’m designing and building model air...
New
PragmaticBookshelf
Tailwind CSS is an exciting new CSS framework that allows you to design your site by composing simple utility classes to create complex e...
New
Exadra37
I am asking for any distro that only has the bare-bones to be able to get a shell in the server and then just install the packages as we ...
New
New
PragmaticBookshelf
Author Spotlight: Tammy Coron @Paradox927 Gaming, and writing games in particular, is about passion, vision, experience, and immersio...
New
PragmaticBookshelf
Author Spotlight: Peter Ullrich @PJUllrich Data is at the core of every business, but it is useless if nobody can access and analyze ...
New
AstonJ
This is cool! DEEPSEEK-V3 ON M4 MAC: BLAZING FAST INFERENCE ON APPLE SILICON We just witnessed something incredible: the largest open-s...
New