This paper use the hotly researched method that combine rely guarantee with separation logic, to verify the concurrent program with memory alloc and dealloc.
Traditinal approaches all depend on reachable analysis, which require a bounded thread number, while this paper use theorem proving approach.
These days, all guys become more and more smart on using theorem proving technology, :)
This is his web site.
What? I found that this paper require user to annotate the code with linearization point, and also need the user to give the semantic of atomic operation in separation logic style.
But one delight point is that this paper dont abstract away the value store in the data structure, as other method do. In this way, some more useful problem can be solved.
BTW: In his previous paper that firstly combine rely/guarentee with seperation logic, there is a concept of stablity, which says something should persist after execut some action, which remind me of the inductive invaraint.
One more notice, this guy also provide ocaml source code on web site.
订阅：
博文评论 (Atom)
博文
没有评论:
发表评论