NB: This Coq documentation contains a revised version of the Coq implementation of these papers [1], [2], [3], [4], and is also the support for ongoing research. A partial archive (14/01/2001) is available at here. Drop us a line if you are interested in a complete, up-to-date archive.

Library topsy_hmAlloc_prg

Require Import bipl.
Require Import expr_b_dp.
Require Import topsy_hm.

Import seplog_Z_m.assert_m.expr_m.
Import seplog_Z_m.

Local Open Scope seplog_expr_scope.
Local Open Scope seplog_cmd_scope.

Definition ENTRYSIZE (x tmp : var.v) :=
  tmp <-* (x -.> next) ;
  tmp <- (var_e tmp .-e var_e x .-e cst_e 2) ;
  ifte (nat_e 0 >> var_e tmp) thendo
    tmp <- nat_e 0
  elsedo
    skip.

Definition findFree (size : nat) (entry fnd sz stts : var.v) :=
  entry <- var_e hmStart;
  stts <-* (entry -.> status);
  fnd <- cst_e 0;
  while.while (var_e entry <>e null &e var_e fnd <>e cst_e 1) (
    stts <-* (entry -.> status);
    ENTRYSIZE entry sz;
    ifte (var_e stts =e Free &e var_e sz >>= nat_e size) thendo
      (fnd <- cst_e 1)
    elsedo
      (entry <-* (entry -.> next))).


original version
Definition compact' (cptr nptr brk tmp cstts nstts : var.v) :=
  while.while (var_e cptr <>e null) (
    nptr <-* (cptr -.> next) ;
    brk <- nat_e 1 ;
    cstts <-* (cptr -.> status) ;
    while.while (var_e cstts =e Free &e var_e nptr <>e null &e var_e brk =e nat_e 1) (
       nstts <-* (nptr -.> status) ;
       ifte (var_e nstts <>e Free) thendo (
          brk <- nat_e 0
       ) elsedo (
         tmp <-* nptr -.> next;
         cptr -.> next *<- var_e tmp ;

         nptr <- (var_e tmp)
       )
    ) ;
    cptr <-* (cptr -.> next)
  ).

optimized version
Definition compact (cptr nptr stts : var.v) :=
  while.while (var_e cptr <>e null) (
    stts <-* (cptr -.> status) ;
    ifte (var_e stts =e Free) thendo (
      nptr <-* (cptr -.> next) ;
      stts <-* (nptr -.> status) ;
      while.while (var_e stts =e Free) (
        stts <-* (nptr -.> next);
        (cptr -.> next) *<- var_e stts ;
        nptr <- var_e stts ;
        stts <-* (nptr -.> status)))
    elsedo
      skip ;
      cptr <-* (cptr -.> next)).

constant
Definition LEFTOVER : nat := 8%nat.


entry contains the address of a free entry, size is the size we want to allocate
Definition split (entry : var.v) (size : nat) (cptr sz : var.v) :=
  ENTRYSIZE entry sz;
  ifte (var_e sz >>= (nat_e size +e nat_e LEFTOVER +e nat_e 2)) thendo (
    cptr <- var_e entry +e nat_e 2 +e nat_e size ;
    sz <-* (entry -.> next) ;
    (cptr -.> next) *<- var_e sz ;
    (cptr -.> status) *<- Free ;
    (entry -.> next) *<- var_e cptr)
   elsedo
     skip
  ;
  (entry -.> status) *<- Allocated.


constants
Definition HM_ALLOCFAILED := cst_e 0.
Definition HM_ALLOCOK := cst_e 1.

alignment calculus ignored (not relevant to verification)
Definition hmAlloc (result : var.v) (size : nat) (entry cptr fnd stts nptr sz : var.v) :=
  
  result <- null;
  findFree size entry fnd sz stts;
  ifte (var_e entry =e null) thendo (
    cptr <- var_e hmStart;
    compact cptr nptr stts;
    findFree size entry fnd sz stts
  ) elsedo
    skip
  ;
  ifte (var_e entry =e null) thendo (
    result <- HM_ALLOCFAILED
  ) elsedo (
    split entry size cptr sz;
    result <- var_e entry +e nat_e 2
  ).