Re: Synchronization Algorithm Verificator for C++0x
On Aug 27, 9:02 pm, Peter Dimov <pdi...@gmail.com> wrote:
On Aug 27, 6:50 pm, "Dmitriy V'jukov" <dvyu...@gmail.com> wrote:
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.programming.threads/msg/07c810b38be80bb=
b
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