The Coq mailing list

["Edward Z. Yang" <ezyang AT MIT.EDU>]

When you need to reason about complex program equivalence involving
state and concurrency, a good proof technique to consider using is
*logical relations* (specifically Kripke logical relations).  If you
are willing to provide some sort of specification which you would
just like to hold the program to, you can use simpler techniques
like what you might find in Bedrock.

Cheers,
Edward

Excerpts from Manjeet Dahiya's message of Wed Aug 14 10:40:12 -0400 2013:
> 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.