This project is read-only.

join_arrays: Is there a way to flush the proof state after calling it?

Jul 19, 2010 at 9:32 PM

Dear all, 

in the code below in function test(big_t *big, a_t *a) I noted that before a memory reinterpretation by join_arrays the snippets containing calls to interfere_a and interfere_c verified quickly (about 6 and 12 seconds at WALLCLOCK1 and WALLCLOCK2) but that the same snippets verified very slowly after use of memory reinterpretation (46 and 52 seconds respectively at WALLCLOCK6 and WALLCLOCK7).Is there any way I could tell vcc to refresh the state after memory reinterpretation so that calls to the interfere_* functions would verify at WALLCLOCK6 and WALLCLOCK7 as fast as at WALLCLOCK1 and WALLCLOCK2?

I apologize that the example is a bit lengthy, it is some memory-manager related memory reinterpretation (here: cast from a container of type a_t containing its value data as unsigned char *rest - a very common structure in operating systems - to byte memory). Despite it looks complicated I have already quite largely simplified it and I guess that the phenomenom can be easily observed by ignoring all those invariants and instead simply lookng in the function test at the places bearing (at the end) the comments WALLCLOCK1, WALLCLOCK2, WALLCLOCK 6, WALLCLOCK7. The memory reinterpretation itself is in the segment terminated by WALLCLOCK4. The fragments terminated by WALLCLOCK3 and WALLCLOCK5 is a simple between two different ghost management structures that have not been deleted to keep the code verifiable but should not need much observation (one could also observe that the section terminated by WALLCLOCK5 is much slower than the section terminated by WALLCLOCK3 but because here the code is slightly different it is not so clear-cut as with the above-mentioned interfere_* calls at WALLCLOCK1,2,6,7).

 

#include "vcc.h"

#define BIG 4096

spec (
typedef vcc(dynamic_owns) struct manager_str {
    unsigned int dummy;
} manager_t; 
)

typedef vcc(dynamic_owns) struct a_str {
    unsigned int dummy;
    unsigned char *rest;
    invariant(rest == (unsigned char*)this + sizeof(struct a_str))
} a_t;

typedef vcc(dynamic_owns) struct big_str {

    unsigned int dummy;

    vcc(dynamic_owns) def_group(ga);
    invariant(set_in(this::ga, owns(this)))
    in_group(ga) spec(manager_t ^man_a;)
    inv_group(ga, keeps(man_a))
    inv_group(ga, forall(a_t *a; set_in(a, owns(man_a)) 
        ==> is_object_root(a)))
    inv_group(ga, forall(a_t *a; set_in(a, owns(man_a)) 
        ==> is_object_root(as_array(a->rest, BIG - sizeof(a_t)))))
    inv_group(ga, forall(a_t *a; set_in(a, owns(man_a)) 
        ==> set_in(as_array(a->rest, BIG - sizeof(a_t)), owns(a))))

    vcc(dynamic_owns) def_group(gchar); 
    invariant(set_in(this::gchar, owns(this)))
    in_group(gchar) spec(manager_t ^man_char;)
    inv_group(gchar, keeps(man_char))
    inv_group(gchar, forall(unsigned char *c; set_in(as_array(c, BIG), owns(man_char)) ==> is_object_root(as_array(c, BIG))))
    
    invariant(man_a != man_char)
    invariant(forall(a_t *a; set_in(a, owns(man_a)) ==> 
        !set_in(as_array((unsigned char*)(void*)a, BIG), owns(man_char))));
    invariant(forall(a_t *c; set_in(as_array(c, BIG), owns(man_char)) ==> 
        !set_in(as_array((a_t *)(void*)c, BIG), owns(man_a))));
} big_t;   

spec(
    vcc(specmacro)
    bool big_wf(big_t *big) returns (
        in_domain(big::gchar, big::gchar) 
        && in_domain(big::ga, big::ga) 
        && (in_domain(big->man_char, big::gchar))
        && (in_domain(big->man_a, big::ga))
        && (big->man_a != big->man_char)
        && (forall(a_t *a; set_in(a, owns(big->man_a)) ==> !set_in(as_array((unsigned char*)(void*)a, BIG), owns(big->man_char))))
        && (forall(a_t *c; set_in(as_array(c, BIG), owns(big->man_char)) ==> 
        !set_in(as_array((a_t *)(void*)c, BIG), owns(big->man_a))))
    );
)


spec (
void interfere_a(manager_t ^manager) 
    maintains(forall(a_t *a; set_in(a, owns(manager)) ==> set_in(as_array(a->rest, BIG - sizeof(a_t)), owns(a))))
    maintains(forall(a_t *a; set_in(a, owns(manager)) ==> is_object_root(as_array(a->rest, BIG - sizeof(a_t)))))
    maintains(forall(a_t *a; set_in(a, owns(manager)) ==> is_object_root(a)))
    maintains(wrapped(manager))
    ensures(set_equal(owns(manager), old(owns(manager))))
    writes(manager)
;
)

spec (
void interfere_c(manager_t ^manager) 
    maintains(forall(unsigned char *c; set_in(as_array(c, BIG), owns(manager)) ==> is_object_root(as_array(c, BIG))))
    maintains(wrapped(manager))
    ensures(set_equal(owns(manager), old(owns(manager))))
    writes(manager)
;
)

void test(big_t *big, a_t *a) 
    writes(big)
    requires(set_in(a, owns(big->man_a)))
    requires(wrapped(big))
{
    assert(in_domain(big, big));

    unwrap(big);
    assert(big_wf(big));
    unwrap(big::gchar);
    speconly ( interfere_c(big->man_char); )
    wrap(big::gchar);
    wrap(big); //WALLCLOCK 1: 6.80s

    unwrap(big);
    assert(big_wf(big));
    unwrap(big::ga);
    speconly ( interfere_a(big->man_a); )
    wrap(big::ga);
    wrap(big); //WALLCLOCK 2: 18.56s

    unwrap(big);
    assert(big_wf(big));
    unwrap(big::ga);
    unwrap(big->man_a);
    giveup_owner(a, big->man_a);
    wrap(big->man_a);
    wrap(big::ga); 
    wrap(big); //WALLCLOCK 3: 28.39s

    unsigned char *c;
    c = (unsigned char *)(void *)a;
    unsigned char *rest;
    rest = a->rest;
    unwrap(a);
    assert(in_domain(as_array(rest, BIG - sizeof(a_t)), 
        as_array(rest, BIG - sizeof(a_t))));
    unwrap(as_array(a->rest, BIG - sizeof(a_t)));
    to_bytes(a);
    join_arrays(as_array(c, sizeof(a_t)), 
        as_array(rest, BIG - sizeof(a_t))); 
    wrap(as_array(c, BIG)); //WALLCLOCK 4: 65.36s

    unwrap(big);
    assert(big_wf(big));
    unwrap(big::gchar);
    unwrap(big->man_char);
    set_owner(as_array(c, BIG), big->man_char);
    wrap(big->man_char);
    wrap(big::gchar);
    wrap(big); //WALLCLOCK 5: 118.69s

    unwrap(big);
    assert(big_wf(big));
    unwrap(big::ga);
    speconly ( interfere_a(big->man_a); )
    wrap(big::ga);
    wrap(big); //WALLCLOCK 6: 164.53s

    unwrap(big);
    assert(big_wf(big));
    unwrap(big::gchar);
    speconly ( interfere_c(big->man_char); )
    wrap(big::gchar);
    wrap(big); //WALLCLOCK 7: 218.97s
}

 

 

 

Regards, Holger