Lune

EuroSys2023Top-tier venue

OFence: Pairing Barriers to Find Concurrency Bugs in the Linux Kernel

Baptiste Lepers, Josselin Giet, Willy Zwaenepoel, Julia Lawall

2023Year
1Citations
2Top-tier citations

Abstract

Knowing which functions may execute concurrently is key to finding concurrency-related bugs. Existing tools infer the possibility of concurrency using dynamic analysis or by pairing functions that use the same locks. Code that relies on more relaxed concurrency controls is, by and large, out of the reach of existing concurrency-related bug-tracking tools.

In this paper, we propose a new heuristic to automatically infer the possibility of concurrency in lockless code that relies on memory barriers (memory fences) for correctness, a task made complex by the fact that barriers do not have a unique identifier and do not have a clearly delimited scope.

To infer the possibility of concurrency between barriers, we propose a novel heuristic based on matching objects accessed before and after barriers. Our approach is based on the observation that barriers work in pairs: if a write memory barrier orders writes to a set of objects, then there should be a read barrier that orders reads to the same set of objects. This pairing strategy allows us to infer which barriers are meant to run concurrently and, in turn, check the code surrounding the barriers for concurrency-related bugs. As a example of a type of concurrency bug, we focus on bugs related to the incorrect placement of reads or writes relative to barriers. When we detect incorrect read or write placements in the code, we automatically produce a patch to fix them.

We evaluate our heuristic on the Linux kernel. Our analysis runs in 8 minutes. We fixed 12 incorrect ordering constraints that could have resulted in hard-to-debug data corruption or kernel crashes. The patches have been merged in the mainline kernel. None of the bugs could have been found using existing static analysis heuristics.

• Software and its engineering → Concurrent programming structures.

Ask about this paper

Your agent reads all of it.

Lune indexed this paper to the last equation, along with the top-tier papers that cite it. Ask a question and the answer quotes them.

Questions to start from

Your agent calls

Luneget_paper_fulltext

Ask in Lune

Free to start. No credit card required.

lune papers fulltext ccec4bf2-dbd5-40ab-8fa3-0a260abac157

Cited by top-tier papers2

Ask how each one uses it

Related papers

Dusk over the sea between two cliffs drawn in fine vertical lines