The Coq mailing list

[Manjeet Dahiya <manjeetdahiya AT gmail.com>]

Hello,

Following is a sample program in the context of concurrent
programming. There are two ways to implement atomic modification of
shared_data. First way is to use lock/mutex and the second one uses
atomic compare-and-swap. The outcome of these two variations is same
i.e. atomic modification of shared_data.

Now my question is much more constrained. So, can we prove equivalence
of programs like this?. Thanks!

void set(int a)
{
  lock(&lk);
  shared_data = a;
  unlock(&lk);
}

void set(int a)
{
  int data;
  while(1)
  {
    int old = shared_data;
    if(cmpxchg(&shared_data, old, a) == old)
      return;
  }
}
--
Manjeet Dahiya
http://manjeetdahiya.com


On Wed, Aug 14, 2013 at 7:44 PM, Nuno Gaspar 
<nmpgaspar AT gmail.com>
 wrote:
> Hello.
>
> Well, generally speaking you'll first need to define what a program is and
> what do you mean by equivalence (I assume you want something more then
> simple syntactical equivalence)
>
> You may want to check Software Foundations, in particular the chapter on
> program equivalence: http://www.cis.upenn.edu/~bcpierce/sf/Equiv.html
>
> Hope it helps.
>
>
> 2013/8/14 
> <manjeetdahiya AT gmail.com>
>
>> Hello,
>>
>> I want to know if coq can be used to prove equivalence of two different
>> programs? Please give me some pointers if it is doable.
>>
>> Thanks!
>
>
>
>
> --
> Bart: Look at me, I'm a grad student, I'm 30 years old and I made $600
> dollars last year.
> Marge: Bart! Don't make fun of grad students, they just made a terrible life
> choice.