Home

Resources, Concurrency and Local Reasoning

Resources, Concurrency and Local Reasoning, Peter O'Hearn, 2007.

Resource has always been a central concern in concurrent programming. Often, a number of processes share access to system resources such as memory, processor time, or network bandwidth, and correct resource usage is essential for the overall working of a system. In the 1960s and 1970s Dijkstra, Hoare and Brinch Hansen attacked the problem of resource control in their basic works on concurrent programming. In addition to the use of synchronization mechanisms to provide protection from inconsistent use, they stressed the importance of resource separation as a means of controlling the complexity of process interactions and reducing the possibility of time-dependent errors. This paper revisits their ideas using the formalism of separation logic.

I have to admit that in posting this paper, I was at least slightly motivated by the imp of the perverse -- it's pretty much a commonplace among expert programmers that reasoning about programs that use shared memory, explicit mutual exclusion, and concurrency is very difficult. So the urge to post a paper showing one approach for doing it in a clean (and imo quite beautiful) way was irresistible.

By neelk at 2007-08-07 08:05 | Parallel/Distributed | other blogs | 7948 reads

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Obsolete

I'd never encountered local reasoning before. It's strange seeing it applied at the global level computer wise (what they call local by splitting up this global environment), instead of on a distributed level. One of the problems of distributed computing is that your programming language features become obsolete. Your data structures need to be serialized and so does your code. Here, they talk about locality such as copying pointers instead of duplicating data. It's unfortunate that it does not talk about abstracting this away and letting the compiler make that determination. Concurrency without distribution is perhaps shortsighted, no? It's certainly a personal opinion, but one that might deserve consideration while doing all this research.

What's even more frightning is that if you apply Hoare's logic to data instead of code, it seems to look ridiculously like data flow and 99% of that paper becomes redundant and obsolete because all those problems have already been solved 30 years ago. I suppose if you're looking for ways to convert current software into concurrent ones, it'd be useful. However, this is as far away from beautiful as you can get.

By Vorlath at Tue, 2007-08-07 20:31 | login or register to post comments

I think there is room for

I think there is room for improvement at all levels of computation, even local ones; I certainly won't complain about local concurrency speedups on my dual core PC, which is arguably a important case at the moment. Distribution is certainly an important consideration, and there is ongoing research on that as well.

By naasking at Tue, 2007-08-07 22:03 | login or register to post comments

As a programmer how can I use this information?

that reasoning about programs that use shared memory, explicit
> mutual exclusion, and concurrency is very difficult

After reading the paper I am not clear on how it becomes easy? Perhaps you can fill in the gap?

By todd at Fri, 2007-08-10 04:51 | login or register to post comments

It doesn't become

It doesn't become easy, but it does become much more systematic. Basically, you've got shared memory, threads, and conditional critical regions as your synchronization mechanism.

Just like in regular imperative code, your big danger is interference -- two parts of your program may both think they have access to some mutable data structure, and then give you garbage by simultaneously mashing on it. The difference with concurrency is "just" that the two interfering blocks of code might be running at the same time.

Now, separation logic comes to the rescue -- it lets you reason about aliasing, and that's exactly what you need in order to ensure that different threads don't mess with the same data. So you take the point of view that a critical section guards some imperative state, and that entering it temporarily transfers ownership of it to you, using the separating conjunction A * B. So locking is a way of transferring ownership of state between threads. So logically, you can move data in and out of different threads, even though there's not necessarily some code representing that transfer in the source.

So you can give clean, elegant proofs of correctness of concurrent imperative programs.

By neelk at Fri, 2007-08-10 08:32 | login or register to post comments