Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Proving equivalence of two different programs

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Proving equivalence of two different programs


Chronological Thread 
  • From: Joey Dodds <jdodds AT princeton.edu>
  • To: t x <txrev319 AT gmail.com>
  • Cc: Kristopher Micinski <krismicinski AT gmail.com>, Manjeet Dahiya <manjeetdahiya AT gmail.com>, Nuno Gaspar <nmpgaspar AT gmail.com>, coq-club <coq-club AT inria.fr>
  • Subject: Re: [Coq-Club] Proving equivalence of two different programs
  • Date: Wed, 14 Aug 2013 11:10:56 -0400

The first two steps t x mentioned are done by CompCert. As of recently, CompCert has a tool clightgen that will take a C program and spit out a .v file containing the AST in Clight (a slightly simplified version of C). From there, it would be sufficient to prove a property on the Clight ast with respect to the CLight semantics (then CompCert guarantees that this property holds on the assembly code that it generates). If we are talking about your sequential program example, and by equality you mean something like  "forall x n, f(x,n) = f'(x,n)" you could prove this by proving both the results of both functions equivalent to the same Gallena function. Our Verifiable C program logic can prove such a specification on a C program.

Joey


On Wed, Aug 14, 2013 at 10:55 AM, t x <txrev319 AT gmail.com> wrote:
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.






Archive powered by MHonArc 2.6.18.

Top of Page