Gc copy

Theory of partial functions.

module partial_function(f,d,r) = {

1) for any x there is at most one y such that f(x,y),

    axiom ~f(X:d,Y:r) | ~f(X:d,Z:r) | Y:r = Z:r

2) dom[f] is the domain of f,

    relation dom[f](X:d)
    axiom ~f(X:d,Y:r) | dom[f](X:d)

3) for any x in dom[f], we have f(x,f[x]).

    schema img[f](x) = ~dom[f](x) | f(x,f[x])

4) This defines how dom[f] updates as we update f:

     update dom[f] from f
       params v:d,w:d in v.f := w ->
        ensures ((~old dom[f](X:d) | dom[f](X:d)) & dom[f](v))
       params v:d in v.f := null ->
        ensures (~old dom[f](X:d) | X:d = v | dom[f](X:d))
       params v:d,w:d in v.f := w.f ->
         ensures (old dom[f](Y:d) & Y:d ~= v | old dom[f](w) & Y:d = v) ->
                      dom[f](Y:d)
}

Type of abstract heap objects

type object

Type of machine addresses

type addr

module hack(f,x,d) = {
    individual f[x] : d
}

instantiate hack(m0,ae1,addr)
instantiate hack(m1,ae1,addr)

relation (X:addr < Y:addr)
relation (X:addr <= Y:addr)

bug 6: forgot to say this:

axiom ~(X < X)
axiom (X < Y & Y < Z) -> (X < Z)
axiom X <= Y <-> (X < Y | X = Y)

bug 10: forgot to say this:

axiom X < Y | X = Y | Y < X

boundaries of from and to regions

individual flo:addr,fhi:addr,tlo:addr,thi:addr

definitions of from and to regions

derived faddr(X:addr) = flo <= X & X < fhi
derived taddr(X:addr) = tlo <= X & X < thi

from and to regions are disjoint

axiom ~(faddr(X) & taddr(X))

bug 5: forgot to say from and to regions can't be empty axiom faddr(flo)

axiom taddr(tlo)

individual temp_addr:addr # TODO: this should be in macro below

macro incr_addr(x) = {
   temp_addr := x;
   x := *;
   assume temp_addr < x;
   assume ~(temp_addr < X & X < x);
   temp_addr := *
}

representation relation between objects and addresses

relation repr(X:object,Y:addr)
instantiate partial_function(repr,object,addr)

the abstract heap

individual hroot:object #root of the abstract heap

each abstract heap cell has two pointer fields

relation h0(X:object,Y:object), h1(X:object,Y:object)
instantiate partial_function(h0,object,object)
instantiate partial_function(h1,object,object)

the machine memory

individual mroot:addr #address of root in machine memory

each machine memory cell has two pointer fields

relation m0(X:addr,Y:addr), m1(X:addr,Y:addr)
instantiate partial_function(m0,addr,addr)
instantiate partial_function(m1,addr,addr)

copied map

relation copied_to(A1:addr,A2:addr)

the representation invariant

macro rep_inv = forall [O1,O2,A1,A2] ( repr(hroot,mroot) & (repr(O1,A1) & h0(O1,O2) -> domm0) & (repr(O1,A1) & h0(O1,O2) & m0(A1,A2) -> repr(O2,A2)) & (repr(O1,A1) & h1(O1,O2) -> domm1) & (repr(O1,A1) & h1(O1,O2) & m1(A1,A2) -> repr(O2,A2)))

init

representation invariant holds initially

  repr(hroot,mroot)
  & (repr(O1,A1) & h0(O1,O2) -> dom[m0](A1))
  & (repr(O1,A1) & h0(O1,O2) & m0(A1,A2) -> repr(O2,A2))
  & (repr(O1,A1) & h1(O1,O2) -> dom[m1](A1))
  & (repr(O1,A1) & h1(O1,O2) & m1(A1,A2) -> repr(O2,A2))

bug 7: repr should be an injection

  & (repr(O1,A1) & repr(O2,A1) -> O1 = O2)

bug 8: initially, repr points only into from region

  & (repr(O1,A1) -> faddr(A1))

  & faddr(mroot)  # root is in "from" region

"from" region is closed

  & ~(m0(A1,A2) & faddr(A1) & ~faddr(A2))
  & ~(m1(A1,A2) & faddr(A1) & ~faddr(A2))
  & ~copied_to(A1,A2)

represenation invarianr

algorithm state variables

individual tnext:addr,talloc:addr

aux variables: TODO: should be local

individual oe1:object,oe2:object,ae1:addr,ae2:addr,a:addr,obj:object,a2:addr

macro copy_obj(fr,to) = {
    to.m0 := fr.m0;
    to.m1 := fr.m1;
    fr.copied_to := to;

bug 4: forgot next lines TODO: need this assertion assert rngrepr;

    obj := *;
    assume repr(obj,fr);
    obj.repr := to;
    instantiate incr_addr(to)
}

macro sweep(field) = {
  a := *;  # TODO: should be a := tnext.field
  a2 := *;
  if (dom[field](tnext)) {
     assume field(tnext,a);

bug 1: had tnext instead of talloc

     if * {
        assume ~copied_to(a,X);

bug 9: was a.field, should have been tnext.field

    tnext.field := talloc;
        instantiate copy_obj(a,talloc)
     }
     else {
        assume copied_to(a,a2);
    tnext.field := a2
     }
  }
}

action initialize = {
  talloc := tlo;  # allocation pointer
  tnext := tlo; # next object to sweep
  instantiate copy_obj(mroot,talloc);

bug 3: forgot next line:

  mroot := tlo;
  hroot.repr := mroot
}

action step = {
  assume tnext < talloc & talloc < thi;
  instantiate sweep(m0);
  instantiate sweep(m1);

bug 2: forgot next line

  instantiate incr_addr(tnext)
}


action error = {
  assume tnext = talloc;

representation invariant does not hold TODO: this should be a macro

  instantiate img[m0](ae1);
  instantiate img[m1](ae1);
  assume ~(
   repr(hroot,mroot)
   & taddr(mroot)
   & (repr(oe1,ae1) & h0(oe1,oe2) & taddr(ae1) -> dom[m0](ae1))
   & (repr(oe1,ae1) & h0(oe1,oe2) & taddr(ae1) & m0(ae1,ae2) -> repr(oe2,ae2) & taddr(ae2))
   & (repr(oe1,ae1) & h1(oe1,oe2) & taddr(ae1) -> dom[m1](ae1))
   & (repr(oe1,ae1) & h1(oe1,oe2) & taddr(ae1) & m1(ae1,ae2) -> repr(oe2,ae2) & taddr(ae2))
   & (repr(oe1,ae1) & repr(oe2,ae1) -> oe1 = oe2)
  )
}

concept spaces from interpolants

concept itp_a = ~dom[repr](hroot)
concept itp_b = ~repr(hroot, mroot)
concept itp_d = ~taddr(mroot)
concept itp_c = (tnext = talloc)
concept itp_e = (talloc = fhi * tnext = fhi * ~repr(hroot, mroot))
concept itp_f = (tnext = talloc * ~repr(hroot, mroot))
concept itp_g = (thi = temp_addr)
concept itp_h = (~taddr(talloc) * talloc < thi)
concept itp_i = (tnext = talloc * ~taddr(talloc))
concept itp_j = (~taddr(tnext))
concept itp_k(V0) = (~dom[m1](tnext) * h1(hroot, V0))
concept itp_l(V1) = (tnext = talloc * h1(hroot, V1))
concept itp_m(V0, V1, V2) = (~repr(V1, V0) * h1(V2, V1) * m1(V0, V0) * repr(V2, V0) * taddr(V0))
concept itp_n(V0, V1) = (talloc = fhi * tnext = fhi * ~repr(hroot, V0) * h1(V1, hroot) * m1(V0, V0) * repr(V1, V0) * taddr(V0))
concept itp_o(V0, V1) = (~dom[m0](V0) * tnext < V0 * h0(V1, V1) * repr(V1, V0))
concept itp_p(V1) = (~dom[m0](talloc) * h0(V1, V1) * repr(V1, talloc))
concept itp_q = (tnext < mroot)
concept itp_r = (tnext = mroot)
concept itp_s(V2) = (talloc < flo * h0(V2, obj) * m0(talloc, talloc) * repr(V2, talloc))
concept itp_t(V3) = (talloc < thi * h0(V3, obj) * m0(thi, talloc) * repr(V3, thi))
concept itp_u(V3) = (talloc < thi * h0(V3, hroot) * m0(thi, talloc) * repr(V3, thi))
concept itp_v(V0, V2) = (thi = flo * V0 < flo * h0(V2, hroot) * m0(V0, V0) * repr(V2, V0))
concept itp_w(V2) = (talloc < flo * h0(V2, hroot) * m0(talloc, talloc) * repr(V2, talloc))
concept itp_x(V3) = (talloc < thi * h0(V3, hroot) * m0(talloc, talloc) * repr(V3, talloc))
concept itp_y(V1, V4, V2) = (V2 < thi * tnext < V2 * h0(V4, hroot) * m0(V1, V2) * repr(V4, V1))
concept itp_z(V2, V0) = (tnext = talloc * h0(V2, hroot) * m0(V0, talloc) * repr(V2, V0))
concept itp_a0 = (tnext < temp_addr)
concept itp_b0(V0, V1) = (~dom[m1](V0) * tnext < V0 * h1(V1, V1) * repr(V1, V0))
concept itp_c0(V0) = (V0 < tnext * taddr(V0))
concept itp_e0(V0, V1, V2) = (V0 < tnext * h0(V1, V2) * repr(V1, V0) * ~dom[m0](V0))
concept itp_e1(V0, V1, V2) = (V0 < tnext * h1(V1, V2) * repr(V1, V0) * ~dom[m1](V0))