Dmitriy - have you researched Checkfence @ Penn State

[Kimo Crossman]

and how it compares with Relay Race Detector?

http://checkfence.sourceforge.net/

www.cis.upenn.edu/~alur/Talks/milner08.ppt

www.cis.upenn.edu/~alur/Talks/ucla07.ppt

www.cis.upenn.edu/acg/talks/pldi07_checkfence_talk.ppt

On Tue, Feb 17, 2009 at 12:38 PM, Dmitriy V'jukov <dvy...@gmail.com> wrote:

On Feb 17, 11:21 pm, Landmann <landmann_...@gmx.de> wrote:

> All right then, I did not realize that the problem of
> inconsistent data is also inherent in the original implementation.
> Thanks for pointing it out! I withdraw my objection.

Ok, no problem, you are always welcomed.


--
Dmitry V'jukov

[Dmitriy Vyukov]

On Dec 10, 10:51 am, Kimo Crossman <k...@webnetic.net> wrote:
> and how it compares with Relay Race Detector?
>
> http://checkfence.sourceforge.net/
>

> <http://checkfence.sourceforge.net/>www.cis.upenn.edu/~alur/Talks/milner08.ppt
>
> <http://www.cis.upenn.edu/~alur/Talks/milner08.ppt>www.cis.upenn.edu/~alur/Talks/ucla07.ppt
>
> www.cis.upenn.edu/acg/talks/pldi07_
> <goog_1260407957268>*checkfence<goog_1260407957268>
> *_talk.ppt </>

[I guess this one must go to the Relacy group, so I cc it.]

Hi Kimo,

Yes, I had researched CheckFence a bit before started work on Relacy.
The main two things that forced me to turn away from CheckFence are:
1. It supports only limited subset of C language. And what I want to
verify is production C/C++ with all these templates, unions,
externally compiled code, thread-local storage, dynamic thread
creation, various OS APIs and whatever.
2. Memory model supported by CheckFence is *very* limited. They only
support atomic operations (I guess fully sequentially consistent) and
4 types of fences. I identified that as "not enough" for real-life
development. Once can't model neither C++0x memory model nor most of
the hardware memory models with it.

--
Dmitriy V'jukov