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.

Popular General Dev topics Top

PragmaticBookshelf
A book on mazes? Seriously? Yes! Because it’s fun. Remember when programming used to be fun? Explore a dozen algorithms for generating th...
New
AstonJ
You might be thinking we should just ask who’s not using VSCode :joy: however there are some new additions in the space that might give V...
New
First poster: mafinar
The following languages will help current and new web developers navigate the programming landscape to code web-based services and apps t...
New
New
AstonJ
Inspired by some of the comments in our https://forum.devtalk.com/t/your-vim-tips/4748 (in particular those by Mafinar and Hallski) …what...
New
OvermindDL1
What shell(s) do you use, why do you use them, and how do you have them configured? Note, this is about shell’s, not terminals, terminal...
New
First poster: dwaynebradley
Maybe it’s just my experience, but Object-Oriented Programming seems like a default, most common paradigm of software engineering. The on...
New
Maartz
Hi folks, I don’t know if I saw this here but, here’s a new programming language, called Roc Reminds me a bit of Elm and thus Haskell. ...
New
Sylvia
About talentbay Our online networking platform connects students with teams in business and industry. It consists of our mobile app for ...
New
First poster: dimitarvp
Rails is not written in Ruby. I’m born and raised in Kraków, a beautiful city in Poland, maybe you’ve heard about it, maybe you’ve even ...
New

Other popular topics Top

AstonJ
A thread that every forum needs! Simply post a link to a track on YouTube (or SoundCloud or Vimeo amongst others!) on a separate line an...
New
malloryerik
Any thoughts on Svelte? Svelte is a radical new approach to building user interfaces. Whereas traditional frameworks like React and Vue...
New
brentjanderson
Bought the Moonlander mechanical keyboard. Cherry Brown MX switches. Arms and wrists have been hurting enough that it’s time I did someth...
New
DevotionGeo
I know that -t flag is used along with -i flag for getting an interactive shell. But I cannot digest what the man page for docker run com...
New
AstonJ
Curious to know which languages and frameworks you’re all thinking about learning next :upside_down_face: Perhaps if there’s enough peop...
New
Rainer
My first contact with Erlang was about 2 years ago when I used RabbitMQ, which is written in Erlang, for my job. This made me curious and...
New
foxtrottwist
Here’s our thread for the Keyboardio Atreus. It is a mechanical keyboard based on and a slight update of the original Atreus (Keyboardio ...
New
Exadra37
On modern versions of macOS, you simply can’t power on your computer, launch a text editor or eBook reader, and write or read, without a ...
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
First poster: joeb
The File System Access API with Origin Private File System. WebKit supports new API that makes it possible for web apps to create, open,...
New