User: Password:
|
|
Subscribe / Log in / New account

Process calculus... will not eliminate bugs

Process calculus... will not eliminate bugs

Posted Feb 24, 2010 3:28 UTC (Wed) by dps (subscriber, #5725)
In reply to: 2.6.32.9 Release notes by nix
Parent article: 2.6.32.9 Release notes

I know quite a bit about process calculus, although my choice of poison is CSP. The concurrency workbench is CCS, if I remember correctly. FDR, which may be available to developers in academia, handles CSP. Do you know of anything similar for pi-calculus?

You could, of course, follow my PhD thesis and prove a general result about a class of systems and limit yourself to that class of system. You can even write frameworks which make it almost impossible to do anything else. (I could say more but wont.)

Unfortunately whatever you do there is the problem of arguing that the kernel code corresponds to the process calculus or has the things your general proof required.

99.98% of the time concurrency just adds locking and context switches and therefore reduces system performance. The best approach the other 0.02% of the time is a more difficult question.


(Log in to post comments)

Process calculus... will not eliminate bugs

Posted Feb 24, 2010 8:30 UTC (Wed) by nix (subscriber, #2304) [Link]

Unfortunately whatever you do there is the problem of arguing that the kernel code corresponds to the process calculus or has the things your general proof required.
Exactly. Without an automated prover the thing is mostly useless for actually reducing bug count: and when was the last time you encountered an automated prover for any but the most toy of languages that actually was automated? They tend to need so much assistance that they become far more a burden than a help, unless you're doing something hyper-life-critical.

I was musing on the theoretical bound when I should have been thinking about reality...


Copyright © 2018, Eklektix, Inc.
Comments and public postings are copyrighted by their creators.
Linux is a registered trademark of Linus Torvalds