The Coq mailing list

[Kristopher Micinski <krismicinski AT gmail.com>]

If you're asking if Coq can automatically take such a program and reify it into the Coq language, then use some decision procedure to solve it, the answer is no.

This type of problem is not a good fit for Coq.  Coq is intended for reasoning about functions with a mix of higher order computation and proof terms, not first order terms with concurrent semantics.

This is not to say that you couldn't code up a semantics for concurrent programs, but what I see here would be extremely complicated: you have to reason about the low level complexities (along the lines of the Bedrock or YNot libraries) but also concurrency.  I don't know of any Coq development which handles these types of programs.

So the answer is technically yes, but practically no, unless you're willing to do an extreme amount of development.

You'd be much better off suited to use a model checker.

Kris

On Wed, Aug 14, 2013 at 10:28 AM, Manjeet Dahiya <manjeetdahiya AT gmail.com> wrote:

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.