Thursday, April 01, 2010

QED simplifies the concurrent program iteratively!

''Since reasoning about complicated thread interleavings is difficult, QED simply avoids reasoning about them! Instead, QED simplifies the concurrent program iteratively, eliminating concurrency in favor of nondeterminism, producing in the limit a nondeterministic sequential program.
... an appropriate combination of these rewrite rules can often simplify concurrent programs dramatically.
'' [source and video]

And a powerpoint presentation: here.

2 comments:

limaCAT said...

The real april fools here is to expect programmers to write pre-conditions and assertions :D.

No, seriously though, I can see this being used in environments like building kernels (Microsoft is doing a LOT of work on concurrency related issues, expecially for the next generation kernels and browsers)or building graphic-intensive videogaming libraries, not for day-to-day business work (even if that would benefit A LOT developers and customers in that environment, not software companies).

Andrea Valente said...

Actually multi-core programming has many of the same problems as concurrent programming... so if they can simplify concurrency we might all (later) benefit in the form of better code for our (now underused) multi-core machine ;)

Post a Comment