Efficient static race detection [closed]

Question

Closed. This question is off-topic. It is not currently accepting answers.

---

Questions asking us to find or recommend tools, libraries, programming languages, resources (including books, blogs, tutorials, and examples), or projects to undertake are off-topic here as they attract opinionated answers that won't have lasting value to others. You may be able to get help in The Whiteboard, our chat room.

Closed 2 years ago.

Improve this question

I am supervising a university project on the topic of race detection for multi-threaded processes with shared memory.

We have a complex algorithm consisting of tens of thousands of subtasks, and we are given a dependency graph over these subtasks. Our goal is to ensure that the output of the algorithm is deterministic, and not dependent on the choices made by the scheduler during runtime. To this end, whenever two processes access the same memory location, we want them to always do it in the same order.

For our purposes, it is not sufficient to say that the algorithm almost always runs deterministically, and we also don't want to suddenly find out that there is a problem during runtime. What we want is a mathematical guarantee that the algorithm runs deterministically. The challenge is to check this efficiently.

Since this is a university project, to some extent both I and my student are in over our heads: Neither of us has any industry experience. Before embarking on the project, we want to understand how such a problem would be tackled in the industry.

Looking at Wikipedia and various academic papers seems to indicate that our situation is uncommon. Most approaches to race detection either use locks, which eliminate races but do not guarantee (as far as we understand) a deterministic output, or operate during runtime (e.g. dynamic race detection algorithms).

• Caleth: At a high level, are you wanting a function isDeterministic :: DependancyGraph -> Bool or a function makeDeterministic :: DependancyGraph -> DependancyGraph?
• Zur Luria: We want to identify the problem. That is, given the dependency graph, we want to either say: 1) This algorithm is deterministic, or 2) This algorithm is not deterministic, because subtasks A and B can access memory location C in different orders (A can precede B or B can precede A).
• Bart van Ingen Schenau: @ZurLuria, the industry standard is to be conservative: Assume the algorithm is non-deterministic unless there is easy proof otherwise and take appropriate measures to ensure/force determinism where it might be needed.
• amon: A simple O(n²) algorithm: let the jobs have a partial order (derived from dependency graph). Let every job have a set of accessed memory locations. For every pair a, b of jobs, if the ordering relation exists, they have no conflict. If no ordering relation exists, check whether memory locations intersect. If so, potential conflict is found, and schedules might be nondeterministic.
• Jörg W Mittag: @ZurLuria: "Just to ask what happens in the real world when people deal with these issues" – 1.) Ignore it. 2.) Ask a scientist for a solution.

Answer 1

we want to understand how such a problem would be tackled in the industry

The typical approach is to either avoid shared memory in the first place, using things like immutable data structures. Or ensuring execution of critical sections are ordered, by using locks, and making sure the behavior of code is correct regardless of ordering. Ensuring thread safety is much more complicated than this, but in most cases it is possible to use patterns and libraries that greatly reduces the risk of problems.

It also involves things like code reviews and lots of testing to find bugs. After all, it is usually not possible to prove that a program is correct, or even to rigorously define what 'correct' is. In most cases, the only thing that matters is that the program is useful for some particular purpose.

I have no idea how to solve the actual problem, I suspect it will be either unsolvable, or exponential in time. But I'm just a developer, I'm sure you know more about the theoretical aspects than me.

I suspect a fundamental problem is that you cannot determine what memory a function will use without knowing the input to the function. And you cannot determine the input without actually running all preceding steps in the program. So I cannot see how you can take a general program and create a graph of subtasks and know what memory each subtask will use in the first place. At least not statically.

And if you force the user to declare these things I'm not sure it will be any better than the current practices.