Library topsy_hmAlloc_prg
Require Import ssreflect.
From mathcomp Require Import eqtype.
Require Import bipl.
Require Import expr_b_dp.
Require Import topsy_hm.
Require Import ZArith.
Import seplog_Z_m.assert_m.expr_m.
Import seplog_Z_m.
Local Open Scope seplog_expr_scope.
Local Open Scope seplog_cmd_scope.
Local Open Scope Z_scope.
Definition ENTRYSIZE (x tmp : var.v) :=
tmp <-* x -.> next ;
tmp <- var_e tmp \- var_e x \- cst_e 2;
If (nat_e 0 \> var_e tmp) Then
tmp <- nat_e 0
Else
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 \!= null \&& var_e fnd \!= cst_e 1) (
stts <-* (entry -.> status);
ENTRYSIZE entry sz;
If (var_e stts \= Free \&& var_e sz \>= nat_e size) Then
(fnd <- cst_e 1)
Else
(entry <-* (entry -.> next))).
From mathcomp Require Import eqtype.
Require Import bipl.
Require Import expr_b_dp.
Require Import topsy_hm.
Require Import ZArith.
Import seplog_Z_m.assert_m.expr_m.
Import seplog_Z_m.
Local Open Scope seplog_expr_scope.
Local Open Scope seplog_cmd_scope.
Local Open Scope Z_scope.
Definition ENTRYSIZE (x tmp : var.v) :=
tmp <-* x -.> next ;
tmp <- var_e tmp \- var_e x \- cst_e 2;
If (nat_e 0 \> var_e tmp) Then
tmp <- nat_e 0
Else
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 \!= null \&& var_e fnd \!= cst_e 1) (
stts <-* (entry -.> status);
ENTRYSIZE entry sz;
If (var_e stts \= Free \&& var_e sz \>= nat_e size) Then
(fnd <- cst_e 1)
Else
(entry <-* (entry -.> next))).
original version
Definition compact' (cptr nptr brk tmp cstts nstts : var.v) :=
while.while (var_e cptr \!= null) (
nptr <-* (cptr -.> next) ;
brk <- nat_e 1 ;
cstts <-* (cptr -.> status) ;
while.while (var_e cstts \= Free \&& var_e nptr \!= null \&& var_e brk \= nat_e 1) (
nstts <-* (nptr -.> status) ;
If (var_e nstts \!= Free) Then (
brk <- nat_e 0
) Else (
tmp <-* nptr -.> next;
cptr -.> next *<- var_e tmp ;
nptr <- (var_e tmp)
)
) ;
cptr <-* (cptr -.> next)
).
while.while (var_e cptr \!= null) (
nptr <-* (cptr -.> next) ;
brk <- nat_e 1 ;
cstts <-* (cptr -.> status) ;
while.while (var_e cstts \= Free \&& var_e nptr \!= null \&& var_e brk \= nat_e 1) (
nstts <-* (nptr -.> status) ;
If (var_e nstts \!= Free) Then (
brk <- nat_e 0
) Else (
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 \!= null) (
stts <-* (cptr -.> status) ;
(If (var_e stts \= Free) Then (
nptr <-* (cptr -.> next) ;
stts <-* (nptr -.> status) ;
while.while (var_e stts \= Free) (
stts <-* (nptr -.> next);
(cptr -.> next) *<- var_e stts ;
nptr <- var_e stts ;
stts <-* (nptr -.> status)))
Else
skip) ;
cptr <-* (cptr -.> next)).
while.while (var_e cptr \!= null) (
stts <-* (cptr -.> status) ;
(If (var_e stts \= Free) Then (
nptr <-* (cptr -.> next) ;
stts <-* (nptr -.> status) ;
while.while (var_e stts \= Free) (
stts <-* (nptr -.> next);
(cptr -.> next) *<- var_e stts ;
nptr <- var_e stts ;
stts <-* (nptr -.> status)))
Else
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;
(If (var_e sz \>= (nat_e size \+ nat_e LEFTOVER \+ nat_e 2)) Then (
cptr <- var_e entry \+ nat_e 2 \+ nat_e size ;
sz <-* (entry -.> next) ;
(cptr -.> next) *<- var_e sz ;
(cptr -.> status) *<- Free ;
(entry -.> next) *<- var_e cptr)
Else
skip)
;
(entry -.> status) *<- Allocated.
ENTRYSIZE entry sz;
(If (var_e sz \>= (nat_e size \+ nat_e LEFTOVER \+ nat_e 2)) Then (
cptr <- var_e entry \+ nat_e 2 \+ nat_e size ;
sz <-* (entry -.> next) ;
(cptr -.> next) *<- var_e sz ;
(cptr -.> status) *<- Free ;
(entry -.> next) *<- var_e cptr)
Else
skip)
;
(entry -.> status) *<- Allocated.
constants
Definition HM_ALLOCFAILED := cst_e 0.
Definition HM_ALLOCOK := cst_e 1.
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;
(If (var_e entry \= null) Then (
cptr <- var_e hmStart;
compact cptr nptr stts;
findFree size entry fnd sz stts
) Else
skip)
;
If (var_e entry \= null) Then (
result <- HM_ALLOCFAILED
) Else (
split entry size cptr sz;
result <- var_e entry \+ nat_e 2
).
result <- null;
findFree size entry fnd sz stts;
(If (var_e entry \= null) Then (
cptr <- var_e hmStart;
compact cptr nptr stts;
findFree size entry fnd sz stts
) Else
skip)
;
If (var_e entry \= null) Then (
result <- HM_ALLOCFAILED
) Else (
split entry size cptr sz;
result <- var_e entry \+ nat_e 2
).