Ralf's Ramblings: Research

Jun 10, 2021 • Research, RustEditsPermalink

A podcast about GhostCell

I recently got asked to appear as a guest on the podcast Building with Rust to talk about our recent work on GhostCell. I never was a guest on a podcast before, so this was very exciting and of course I said yes. :) That episode has been released now, so you can listen to an hour of me talking about GhostCell and about PL research more generally:

Ralf Jung on GhostCell and Working as a PL Researcher

Have fun, and I am sorry for talking so fast. ;)

Read more...

Mar 23, 2021 • Research, RustEditsPermalink

Safe Systems Programming in Rust

It has been a long time coming; now our Communications of the ACM article Safe Systems Programming in Rust has finally been published. A pdf version is also available. We explain at a high level what makes Rust so innovative and interesting, and how we are studying Rust formally in the RustBelt project. The ACM even produced a short video which includes Derek and me explaining the main points of the article. Have fun. :)

Read more...

Dec 14, 2020 • Research, RustEditsPermalink

Pointers Are Complicated II, or: We need better language specs

Some time ago, I wrote a blog post about how there’s more to a pointer than meets the eye. One key point I was trying to make is that

just because two pointers point to the same address, does not mean they are equal in the sense that they can be used interchangeably.

This “extra information” that distinguishes different pointers to the same address is typically called provenance. This post is another attempt to convince you that provenance is “real”, by telling a cautionary tale of what can go wrong when provenance is not considered sufficiently carefully in an optimizing compiler. The post is self-contained; I am not assuming that you have read the first one. There is also a larger message here about how we could prevent such issues from coming up in the future by spending more effort on the specification of compiler IRs.

Read more...

Sep 3, 2020 • Research, RustEditsPermalink

Achievement 'PhD' unlocked

It is done! My dissertation is finally complete. So if you always wanted an in-depth account of my research on Rust (and more), you can go read my dissertation. With its almost 300 pages, it should keep you busy for a while. ;)

Read more...

Nov 18, 2019 • Research, RustEditsPermalink

Stacked Borrows: An Aliasing Model for Rust (the paper)

I have blogged a few times before about Stacked Borrows, my proposed aliasing model for Rust. But I am a researcher, and what researchers (are expected to) do is write papers—so that’s what we did for Stacked Borrows as well. After a lot of work, I can now finally present to you our paper Stacked Borrows: An Aliasing Model for Rust (thanks to open access, the paper is available under the CC-BY 4.0 license).

Read more...

Oct 20, 2019 • Research, RustEditsPermalink

What Type Soundness Theorem Do You Really Want to Prove?

My advisor Derek and some of my coauthors Amin, Robbert and Lars just put out a blog post on the SIGPLAN blog on the idea of “semantic typing”. This is the methodology behind RustBelt, so the post is a great starting point for understanding the context of that paper and the key bits of prior research that it rests on. In fact they used Rust as their main example language for that post, and I helped them out a bit with some of the technical details there so they kindly added me to the author list.

The approach they describe is much more widely applicable than Rust though; it provides a whole new perspective on type systems that I think deserves way more attention than it gets. If you are interested in formal methods for type systems and in particular for Rust, you should check it out! It’s a great read:

“What Type Soundness Theorem Do You Really Want to Prove?” on PL Perspectives

Read more...

Jul 14, 2019 • Research, RustEditsPermalink

"What The Hardware Does" is not What Your Program Does: Uninitialized Memory

This post is about uninitialized memory, but also about the semantics of highly optimized “low-level” languages in general. I will try to convince you that reasoning by “what the hardware does” is inherently flawed when talking about languages such as Rust, C or C++. These are not low-level languages. I have made this point before in the context of pointers; this time it is going to be about uninitialized memory.

The trigger for this post is the deprecation of mem::uninitialized() with Rust 1.36, but the post is just as relevant for C/C++ as it is for Rust.1

  1. This deprecation has been in the works for more than two years, and it has been almost a year since I took over pushing for this. I am very happy that we are finally there! 

Read more...

May 21, 2019 • Research, RustEditsPermalink

Putting the stack back into Stacked Borrows

Less than a month ago, I announced Stacked Borrows 2. In particular, I hoped that that version would bring us closer to proper support for two-phase borrows. Turns out I was a bit too optimistic! Last week, @Manishearth asked on Zulip why Miri rejected a certain program, and it turned out that the issue was related to two-phase borrows: in combination with interior mutability, behavior wasn’t always what we wanted it to be. So, I went back to the drawing board and tried to adjust Stacked Borrows.

In the end, I decided to give up on “proper” support for two-phase borrows for now, which I explained here. But I also made some tweaks to Stacked Borrows that affect all accesses (not just two-phase borrows), and that’s what this post is about. I am referring to this as “Stacked Borrows 2.1”.

Read more...

May 15, 2019 • Coq, ResearchEditsPermalink

Exponential blowup when using unbundled typeclasses to model algebraic hierarchies

When formalizing a proof in an interactive theorem prover like Coq, one reoccurring issue is the handling of algebraic hierarchies. Such hierarchies are everywhere: some operations are associative, while others commute; some types have an equivalence relation, while others also have a (pre-)order or maybe even a well-ordering; and so on. So the question arises: What is the best way to actually encode these hierarchies in Coq? Coq offers two mechanisms that are suited to solve this task: typeclasses and canonical structures. Both can be instrumented in different ways to obtain a (more or less) convenient-to-use algebraic hierarchy. A common approach using typeclasses is the “unbundled” approach by Bas Spitters and Eelis van der Weegen. However as we learned the hard way in the Coq formalization of the original Iris paper, this approach quickly leads to terms that seem to be exponential in size. In this post, I will explain the cause of this exponential blowup.

Read more...

Apr 30, 2019 • Research, RustEditsPermalink

Stacked Borrows 2

Recently, I have significantly updated Stacked Borrows in order to fix some issues with the handling of shared references that were uncovered in the previous version. In this post, I will describe what the new version looks like and how it differs from Stacked Borrows 1. I assume some familiarity with the prior version and will not explain everything from scratch.

Read more...

Dec 12, 2018 • Rant, ResearchEditsPermalink

Google Scholar Considered Harmful

I am currently applying for academic positions, and several people recommended I get a Google Scholar profile because hiring committees will look for that. I even found one vacancy that explicitly requested submitting a Google Scholar profile alongside the application. Google Scholar provides not just a list of publications (which is of course part of the application, and which is also available on dblp), but also a citation count and computation of several publication-related indices. This post is about why I don’t have a Google Scholar profile (yet).

Read more...

Jul 13, 2018 • Research, RustEditsPermalink

The Tale of a Bug in Arc: Synchronization and Data Races

While I was busy doing Rust-unrelated research, RustBelt continues to move and recently found another bug (after a missing impl !Sync that we found previously): It turns out that Arc::get_mut did not perform sufficient synchronization, leading to a data race.

Notice that I am just the messenger here, the bug was actually found by Hai and Jacques-Henri. Still, I’d like to use this opportunity to talk a bit about weak memory, synchronization and data races. This is just a primer, there are tons of resources on the web that go into more detail (for example here).

Read more...

Apr 10, 2018 • Research, RustEditsPermalink

Safe Intrusive Collections with Pinning

In my last post, I talked about the new “pinned references” which guarantee that the data at the memory it points to will not, ever, be moved elsewhere. I explained how they enable giving a safe API to code that could previously only be exposed with unsafe, and how one could go about proving such a thing. This post is about another application of pinned references—another API whose safety relies on the pinning guarantees: Intrusive collections. It turns out that pinned references can almost be used for this, but not quite. However, this can be fixed by extending the guarantees provided by pinned references, as suggested by @cramertj.

Read more...

Apr 5, 2018 • Research, RustEditsPermalink

A Formal Look at Pinning

Recently, a new API for “pinned references” has landed as a new unstable feature in the standard library. The purpose of these references is to express that the data at the memory it points to will not, ever, be moved elsewhere. @withoutboats has written about how this solves a problem in the context of async IO. In this post, we take a closer, more formal look at that API: We are going to take a stab at extending the RustBelt model of types with support for pinning.

Read more...

Jan 31, 2018 • Research, RustEditsPermalink

Sharing for a Lifetime

This post is about an aspect of the RustBelt paper. Concretely, I’d like to share some of our thoughts on the nature of types and shared references. Let’s see how well this goes. :)

Shared references are an extremely powerful mechanism in the Rust type system, and we’ve had quite some trouble finding a good way of handling them in our formal model. In this post, I will present the model that we came up with.

Read more...

Jan 21, 2018 • Research, RustEditsPermalink

RustBelt Conference Talk

Last week, I was in Los Angeles at POPL 2018 to present our paper RustBelt: Securing the Foundations of the Rust Programming Language. The talk has been recorded, so if you want to get a 20-minute summary of the paper, go watch it on YouTube. If you have any questions, feel free to join the forum thread linked below :)

Read more...

Dec 15, 2017 • ResearchEditsPermalink

Interview for People of Programming Languages

POPL 2018, the conference where I will present our RustBelt paper, is doing a series of interviews with senior and junior people from the community: People of Programming Languages. They also asked me if I wanted to be part of this, and of course I accepted. This was the first time I was asked to give an interview, so needless to say, I was super excited! I got the opportunity to talk about how I came to do research in PL, what my research is about, and ramble a bit about why I think Coq is great. If you want to read more, check out my interview. Be sure to also have a look at the other interviews.

Thanks a lot to Jean Yang, the Publicity Chair for POPL 2018, for making this a very pleasant experience. (Though, as you can see, I had to send them a picture, which was certainly the least pleasant part of this. ;)

PS: It seems I have consistent bad luck with my POPL talk slots, because my talk is again in the very last session of the conference. This time, in fact, it’s the very last talk of the main track. Maybe some people read this interview and consider staying anyway :D

Read more...

Jul 8, 2017 • Research, RustEditsPermalink

RustBelt: Securing the Foundations of the Rust Programming Language

Just yesterday, we submitted our paper RustBelt: Securing the Foundations of the Rust Programming Language. Quoting from the abstract:

Rust is a new systems programming language that promises to overcome the seemingly fundamental tradeoff between high-level safety guarantees and low-level control over resource management. Unfortunately, none of Rust’s safety claims have been formally proven, and there is good reason to question whether they actually hold. Specifically, Rust employs a strong, ownership-based type system, but then extends the expressive power of this core type system through libraries that internally use unsafe features. In this paper, we give the first formal (and machine-checked) safety proof for a language representing a realistic subset of Rust. Our proof is extensible in the sense that, for each new Rust library that uses unsafe features, we can say what verification condition it must satisfy in order for it to be deemed a safe extension to the language. We have carried out this verification for some of the most important libraries that are used throughout the Rust ecosystem.

Read more...

Jun 9, 2017 • Research, RustEditsPermalink

How MutexGuard was Sync When It Should Not Have Been

A couple of weeks ago, our ongoing effort to formalize Rust’s type system lead to us actually discovering a bug in the Rust standard library: MutexGuard implemented Sync in cases where it should not. This could lead to data races in safe programs. Ouch.

Read more...

Jan 20, 2017 • Research, RustEditsPermalink

Talk @ Paris Rust Meetup

This week, I have been at the Paris Rust Meetup. Meeting all sorts of Rust people was great fun, and the Mozilla offices in Paris are absolutely impressive. You should totally check them out if you have a chance.

On that meetup, I gave a short talk about the current status of my formalization of the Rust type system.

Read more...

Jan 9, 2016 • Research, RustEditsPermalink

The Scope of Unsafe

I’d like to talk about an important aspect of dealing with unsafe code, that still regularly seems to catch people on the wrong foot:

When checking unsafe code, it is not enough to just check the contents of every unsafe block.

The “scope” in the title refers to the extent of the code that has to be manually checked for correctness, once unsafe is used. What I am saying is that the scope of unsafe is larger than the unsafe block itself.

It turns out that the underlying reason for this observation is also a nice illustration for the concept of semantic types that comes up in my work on formalizing Rust (or rather, its type system). Finally, this discussion will once again lead us to realize that we rely on our type systems to provide much more than just type safety.

Update (Jan 11th): Clarified the role of privacy; argued why evil is the problem.

Read more...

Oct 12, 2015 • Research, RustEditsPermalink

Formalizing Rust

My current research project – and the main topic of my PhD thesis – is about developing a semantic model of the Rust programming language and, most importantly, its type system. Rust is an attempt of Mozilla to find a sweet spot in the design space of programming languages: A language that provides low-level resource management (making it a systems language), is convenient for programmers and guards against memory errors and thread unsafety. Other have said and written a lot on why we need such a language, so I won’t lose any more words on this. Let me just use this opportunity for a shameless plug: If you are curious and want to learn Rust, check out Rust-101, a hands-on Rust tutorial I wrote. I am going to assume some basic familiarity with Rust in the following.

Why do we want to do research on Rust? First of all, I’m (becoming) a programming languages researcher, and Rust is an interesting new language to study. It’s going to be fun! Honestly, that’s enough of a reason for me. But there are other reasons: It shouldn’t be a surprise that bugs have been found in Rust. There are lots of things that can be done about such bugs – my take on this is that we should try to prove, in a mathematical rigorous way, that no such bugs exist in Rust. This goes hand-in-hand with other approaches like testing, fuzzing and static analysis. However, we (at my research group) are into formalizing things, so that’s what we are going to do as part of the RustBelt research project.

Update: Added link to RustBelt website.

Read more...