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

New
New
First poster: bot
There is a long, difficult road from vague, pie-in-the-sky ideas about what would be cool to have in a new programming language, to a rob...
New
First poster: bot
A short history of ReScript (BuckleScript). It takes time to write such a post for a non-native speaker like me, but I appreciate what t...
New
First poster: bot
Lisp Interview: questions to Alex Nygren of Kina Knowledge, using Common Lisp extensively in their document processing stack - Lisp jour...
New
CommunityNews
Martin Thompson On How To Manage Software Complexity | The Engineering Room Ep. 4. In this episode, Dave Farley chats with Martin Thomps...
New
CommunityNews
GitHub - let-def/hotcaml: Hotcaml: an interpreter with watching and reloading. Hotcaml: an interpreter with watching and reloading - Git...
New
First poster: bot
Hacking sum types with Go generics. Go doesn’t have sum types, but generics get us one step closer to a useful polyfill. If you’ve ever ...
New
First poster: bot
To build a web application you need to make architecture decisions across a range of topics. The beauty of Ruby on Rails or Django is tha...
New
First poster: herbert
Why Rust should not have provided unwrap. I see the unwrap function called a lot, especially in example code, quick-and-dirty prototype ...
New

Other popular topics Top

Devtalk
Reading something? Working on something? Planning something? Changing jobs even!? If you’re up for sharing, please let us know what you’...
1037 19435 386
New
AstonJ
I’ve been hearing quite a lot of comments relating to the sound of a keyboard, with one of the most desirable of these called ‘thock’, he...
New
AstonJ
Do the test and post your score :nerd_face: :keyboard: If possible, please add info such as the keyboard you’re using, the layout (Qw...
New
DevotionGeo
The V Programming Language Simple language for building maintainable programs V is already mentioned couple of times in the forum, but I...
New
New
PragmaticBookshelf
Author Spotlight James Stanier @jstanier James Stanier, author of Effective Remote Work , discusses how to rethink the office as we e...
New
New
New
PragmaticBookshelf
Explore the power of Ash Framework by modeling and building the domain for a real-world web application. Rebecca Le @sevenseacat and ...
New
PragmaticBookshelf
Fight complexity and reclaim the original spirit of agility by learning to simplify how you develop software. The result: a more humane a...
New