The Coq mailing list

[t x <txrev319 AT gmail.com>]

This is do-able, provided you're willing to put in the time.

You can start out by defining a machine architecture (say formalizing MIPS).

Then, you write a C -> Mips compiler (in Gallina).

After that, you can define "program equivalence" as "runs in the same number of steps + register state identital + memory state identical".

After that, you can state the theorem in Coq, and try to formally prove it.

On Wed, Aug 14, 2013 at 2:41 PM, Kristopher Micinski <krismicinski AT gmail.com> wrote:

For these types of examples you may want to look at libraries like Bedrock, from what I know in my limited experience they handle sequential programs quite well.  I'm not sure of the state for equality checking, however.

Kris

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

Another example, where programs are sequential (no data sharing).

int f'(int x, int n)
{
  int i, k = 0;
  for (i=0; i!=n; ++i){
    x += k;
    k += 5;
    if (i >= 5)
      k += 15;
  }
  return x;
}


int f(int x, int n){
  int i, k = 0;
  for (i=0; i!=n; ++i){
    x += k*5;
    k += 1;
    if (i >= 5)
      k += 3;
  }
  return x;

}
--
Manjeet Dahiya
http://manjeetdahiya.com

On Wed, Aug 14, 2013 at 7:58 PM, 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.