Re: Synchronization Algorithm Verificator for C++0x

[Dmitriy V'jukov]

On 2 Á×Ç, 20:47, "Dmitriy V'jukov" <[e-mail]:

I want to announce tool called Relacy Race Detector, which I've
developed. It's synchronization algorithm verificator for C++0x's
relaxed memory model.

Q: Can I use Relacy Race Detector to check my algo againts other that C
++0x memory models (x86, PPC, Java, CLI)?
A Yes, you can. Fortunately, C++0x memory model is very relaxaed, so
for the main part it's a "superset" of basically any other memory
model. You just have to define "binding" between your target memory
model and C++0x memory model.

Let's create such binding, for example, for x86 memory model:
- plain load operation is always "acquire" (i.e.
memory_order_acquire)
- plain store operation is always "release" (i.e.
memory_order_release)
- atomic RMW operation is always sequentially consistent (i.e.
memory_order_seq_cst)
- mfence instruction is
std::atomic_thread_fence(memory_order_seq_cst)
That is all. You can create such bindings for other hardware memory
models you are interested in (PPC, Itatium, SPARC etc).

And you can define such binding to other abstract memory model, like
Java MM. Let's see:
- plain load is "relaxed" (i.e. memory_order_relaxed)
- plain store is "relaxed" (i.e. memory_order_relaxed)
- volatile load is "acquire" (i.e. memory_order_acquire)
- volatile store operation is "release" (i.e. memory_order_release)
- atomic RMW operation is always sequentially consistent (i.e.
memory_order_seq_cst)
But here are some caveats. First, you have to emulate work of GC, i.e.
put all allocated memory to special list, and free all allocated
memory in test_suite::after(). Second, you have to manually emit
sequentially consistent memory fence between every volatile store and
volatile load. Third, you have to manually initialize all variables to
default value (0). Fourth, there is no such thing as data race, so you
have to define all variables as std::atomic, this will effectively
disable data race detection mechanizm. Well, actually you can use
rl::var variables, if you know that there must be no concurrent
accesses to variable, this will enable some automatic error detection
wrt data races.
Sounds not very cool... So I'm going to add built-in support for Java
and CLI. Then user would have to define something like RL_JAVA_MODE/
RL_CLI_MODE, and get all those things out-of-the-box. But yes, it
still will be C++ library. What do you think?

Dmitriy V'jukov

[Dmitriy V'jukov]

I have uploaded release 1.2 of Relacy Race Detector:
http://groups.google.com/group/relacy/files

The main feature of the release is support for Java/CLI (aka .NET)
algorithm verification (but don't get confused - it's still C++
library).
The support includes following things:
- Emulation of GC: just allocate-and-forget. GC eliminates important
problems associated with lock-free algorithms - safe memory
reclamation and ABA problem. You can use GC and in C++ mode - just
define RL_GC.
- CLI memory model. Stronger atomic RMW operations and stronger
seq_cst fence.
- Java memory model. Stronger atomic RMW operations and stronger
seq_cst fence and seq_cst fence emitted automatically between volatile
store and volatile load.
- Basic CLI API associated with synchronization. rl::nvolatile<>
class emulates CLI volatiles. rl::nvar<emulates plain CLI variables.
Interlocked operations available in rl::Interlocked namespace (i.e.
rl::Interlocked::CompareExchange()). And also
rl::Thread::MemoryBarrier(), rl::Thread::VolatileRead(),
rl::Thread::VolatileWrite() and rl::Thread::SpinWait().
- Basic Java API associated with sycnronization. rl::jvolatile<>,
rl::jvar<>, rl::AtomicInteger and rl::AtomicLong. Note that extensive
Java/CLI support libraries are not emulated (various ConcurrentQueue's
and so on). But you can use mutexes, condition_variables, semaphores
and events from C++ API, POSIX API or Win API.

Example of CLI algorithm verification you can see here:
http://groups.google.com/group/relac...1c913c298a20ab

Java example:
http://groups.google.com/group/relac...7150359b8fb57d

Also release includes a bunch of bug fixes.

Looking forward to your comments.

Dmitriy V'jukov

[Dmitriy V'jukov]

I have uploaded release 1.2 of Relacy Race Detector:
http://groups.google.com/group/relacy/files

Dmitriy V'jukov

[Dmitriy V'jukov]

On Aug 26, 10:38*pm, "Dmitriy V'jukov" <[e-mail]:

The main feature of the release is support for Java/CLI (aka .NET)
algorithm verification (but don't get confused - it's still C++
library).
The support includes following things:
*- Emulation of GC: just allocate-and-forget. GC eliminates important
problems associated with lock-free algorithms - safe memory
reclamation and ABA problem. You can use GC and in C++ mode - just
define RL_GC.
*- CLI memory model. Stronger atomic RMW operations and stronger
seq_cst fence.
*- Java memory model. Stronger atomic RMW operations and stronger
seq_cst fence and seq_cst fence emitted automatically between volatile
store and volatile load.
*- Basic CLI API associated with synchronization. rl::nvolatile<>
class emulates CLI volatiles. rl::nvar<emulates plain CLI variables.
Interlocked operations available in rl::Interlocked namespace (i.e.
rl::Interlocked::CompareExchange()). And also
rl::Thread::MemoryBarrier(), rl::Thread::VolatileRead(),
rl::Thread::VolatileWrite() and rl::Thread::SpinWait().
*- Basic Java API associated with sycnronization. rl::jvolatile<>,
rl::jvar<>, rl::AtomicInteger and rl::AtomicLong. Note that extensive
Java/CLI support libraries are not emulated (various ConcurrentQueue's
and so on). But you can use mutexes, condition_variables, semaphores
and events from C++ API, POSIX API or Win API.

I forgot to mention following moment. There are no such things as data
races and uninitialized variables in Java/CLI. This basically forces
me to disable some types of automatically detectable errors (data
races and accesses to uninitialized variables) in Java/CLI mode. And
from verification point of view this is bad. But in Java/CLI mode you
still can use rl::var<>'s, and this will effectively re-enable
detection of mentioned types of errors. I.e. if you know that some
variable must be accesses only in 'single-threaded way' (for example,
all accesses are protected by mutex), then you can use rl::var<for
this variable.
Dmitriy V'jukov

[Peter Dimov]

On Aug 26, 9:38*pm, "Dmitriy V'jukov" <[e-mail]:

*- Java memory model. Stronger atomic RMW operations and stronger
seq_cst fence and seq_cst fence emitted automatically between volatile
store and volatile load.

What are the goals of this mode?

If it's intended to analyze Java code against the formal Java memory
model, the above description is not correct. Consider again

T1: x = 1;
T2: y = 1;
T3: r1 = x; r2 = y;
T4: r3 = y; r4 = x;

(x, y volatile, initial value 0)

(r1,r2,r3,r4) = (1, 0, 1, 0) is disallowed by the Java memory model,
but allowed by your description.

This mode may be considered correct if it's intended to analyze Java
code running on a typical x86 JVM that follows the cookbook, but these
JVMs do not conform to the Java memory model and will likely be fixed
at some point.

Why not just model volatile loads and stores as volatile loads and
stores, instead of transforming the code and analyzing the transformed
result?

[Peter Dimov]

On Aug 27, 6:50*pm, "Dmitriy V'jukov" <[e-mail]:

Does modeling of Java volatile stores/loads as C++0x seq_cst stores/
loads satisfy those requirements?

I believe that it does.

I don't get you here. There are no such synchronization actions as
volatile loads and stores in C++0x.

Yes, I used the Java meaning of volatile. I meant that Relacy can
directly implement the JMM meaning of volatile for rl::jvolatile,
instead of translating it to C++ terms first. This would allow you to
run the same algorithm expressed in Java and in C++ seq_cst and verify
whether the results match. So Relacy can give us a direct answer to
your first question above. :-)

[Dmitriy V'jukov]

On Aug 27, 9:02*pm, Peter Dimov <[e-mail]:

On Aug 27, 6:50*pm, "Dmitriy V'jukov" <[e-mail]:

Does modeling of Java volatile stores/loads as C++0x seq_cst stores/
loads satisfy those requirements?

I believe that it does.

Good! Than it will be simple.

I don't get you here. There are no such synchronization actions as
volatile loads and stores in C++0x.

Yes, I used the Java meaning of volatile. I meant that Relacy can
directly implement the JMM meaning of volatile for rl::jvolatile,
instead of translating it to C++ terms first. This would allow you to
run the same algorithm expressed in Java and in C++ seq_cst and verify
whether the results match. So Relacy can give us a direct answer to
your first question above. :-)

Hmmm... It looks like vicious circle :)

Direct modeling of Java and CLI synchronization primitives I consider
as last resort. I hope that I will be able to easily model Java/CLI
primitives via C++0x primitives. Currently I add only 2 patches. First
I've described here:
http://groups.google.com/group/comp....c810b38be80bbb
And second is that every atomic RMW is followed by seq_cst fence:
T java_cli_atomic_rmw(...)
{
T r = cpp0x_atomic_rmw(..., memory_order_seq_cst);
cpp0x_atomic_thread_fence(memory_order_seq_cst);
return r;
}
I think that this is intended behavior of CLI Interlocked operations,
because they based on Win32 Interlocked operations, and they are based
on x86 locked instructions :)
I am not sure about Java here. I can't find answer in language
specification and description of atomic package...

Dmitriy V'jukov