coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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:
After that, you can define "program equivalence" as "runs in the same number of steps + register state identital + memory state identical".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 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;
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.
- [Coq-Club] Proving equivalence of two different programs, manjeetdahiya, 08/14/2013
- Re: [Coq-Club] Proving equivalence of two different programs, Kristopher Micinski, 08/14/2013
- Re: [Coq-Club] Proving equivalence of two different programs, Nuno Gaspar, 08/14/2013
- Re: [Coq-Club] Proving equivalence of two different programs, Manjeet Dahiya, 08/14/2013
- Re: [Coq-Club] Proving equivalence of two different programs, Manjeet Dahiya, 08/14/2013
- Re: [Coq-Club] Proving equivalence of two different programs, Kristopher Micinski, 08/14/2013
- Re: [Coq-Club] Proving equivalence of two different programs, t x, 08/14/2013
- Re: [Coq-Club] Proving equivalence of two different programs, Kristopher Micinski, 08/14/2013
- Message not available
- Re: [Coq-Club] Proving equivalence of two different programs, Joey Dodds, 08/14/2013
- Re: [Coq-Club] Proving equivalence of two different programs, t x, 08/14/2013
- Re: [Coq-Club] Proving equivalence of two different programs, Kristopher Micinski, 08/14/2013
- Re: [Coq-Club] Proving equivalence of two different programs, Edward Z. Yang, 08/14/2013
- Re: [Coq-Club] Proving equivalence of two different programs, Manjeet Dahiya, 08/14/2013
- Re: [Coq-Club] Proving equivalence of two different programs, Kristopher Micinski, 08/14/2013
- Re: [Coq-Club] Proving equivalence of two different programs, Manjeet Dahiya, 08/14/2013
Archive powered by MHonArc 2.6.18.