From 9ed0e3efe20cff5dc146543920f61d1b3dccdf51 Mon Sep 17 00:00:00 2001 From: Rini Banerjee Date: Wed, 18 Mar 2026 23:46:07 +0000 Subject: [PATCH 1/4] separate ownership from logical assertion for ByteV and usages --- defs.h | 12 ++++++++---- 1 file changed, 8 insertions(+), 4 deletions(-) diff --git a/defs.h b/defs.h index 9762473..df394b7 100644 --- a/defs.h +++ b/defs.h @@ -291,10 +291,10 @@ predicate void Byte (pointer virt) return; } -predicate void ByteV (pointer virt, u8 the_value) +predicate void ByteV (pointer virt) { take B = Owned(virt); - assert (B == the_value); + // assert (B == the_value); return; } @@ -323,7 +323,9 @@ predicate void ZeroPage (pointer vbase, boolean guard, u8 order) let vbaseI = ((u64) vbase); // FULM_OPT take Bytes = each (u64 i; (vbaseI <= i) && (i < (vbaseI + length))) - {ByteV(array_shift(NULL, i), 0u8)}; + {ByteV(array_shift(NULL, i))}; + assert (each (u64 i; (vbaseI <= i) && (i < (vbaseI + length))) + {Bytes[i] == 0u8}); return; } } @@ -335,7 +337,9 @@ predicate void AllocatorPageZeroPart (pointer zero_start, u8 order) let length = region_length - sizeof; // FULM_OPT take Bytes = each (u64 i; (start <= i) && (i < (start + length))) - {ByteV(array_shift(NULL, i), 0u8)}; + {ByteV(array_shift(NULL, i))}; + assert (each (u64 i; (start <= i) && (i < (start + length))) + {Bytes[i] == 0u8}); return; } From 25402a5efc1db2649e2c789219ffd1755c1d8956 Mon Sep 17 00:00:00 2001 From: Rini Banerjee Date: Wed, 18 Mar 2026 23:56:31 +0000 Subject: [PATCH 2/4] fix up spec so it still runs as expected --- defs.h | 15 +++++++++++---- 1 file changed, 11 insertions(+), 4 deletions(-) diff --git a/defs.h b/defs.h index df394b7..1f561ce 100644 --- a/defs.h +++ b/defs.h @@ -291,13 +291,20 @@ predicate void Byte (pointer virt) return; } -predicate void ByteV (pointer virt) +predicate void ByteV (pointer virt, u8 the_value) { take B = Owned(virt); - // assert (B == the_value); + assert (B == the_value); return; } +predicate (u8) NewByteV (pointer virt) +{ + take B = Owned(virt); + // assert (B == the_value); + return B; +} + predicate void Page (pointer vbase, boolean guard, u8 order) { if (!guard) { @@ -323,7 +330,7 @@ predicate void ZeroPage (pointer vbase, boolean guard, u8 order) let vbaseI = ((u64) vbase); // FULM_OPT take Bytes = each (u64 i; (vbaseI <= i) && (i < (vbaseI + length))) - {ByteV(array_shift(NULL, i))}; + {NewByteV(array_shift(NULL, i))}; assert (each (u64 i; (vbaseI <= i) && (i < (vbaseI + length))) {Bytes[i] == 0u8}); return; @@ -337,7 +344,7 @@ predicate void AllocatorPageZeroPart (pointer zero_start, u8 order) let length = region_length - sizeof; // FULM_OPT take Bytes = each (u64 i; (start <= i) && (i < (start + length))) - {ByteV(array_shift(NULL, i))}; + {NewByteV(array_shift(NULL, i))}; assert (each (u64 i; (start <= i) && (i < (start + length))) {Bytes[i] == 0u8}); return; From c8ae7a75a54c4534bf2df9f7f1911790108a3eac Mon Sep 17 00:00:00 2001 From: Rini Banerjee Date: Sun, 22 Mar 2026 19:59:33 +0000 Subject: [PATCH 3/4] Replace calls to NewByteV with RW Makes Fulm analysis for perf optimisation marginally simpler --- defs.h | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/defs.h b/defs.h index 1f561ce..a78a2a3 100644 --- a/defs.h +++ b/defs.h @@ -298,12 +298,12 @@ predicate void ByteV (pointer virt, u8 the_value) return; } -predicate (u8) NewByteV (pointer virt) -{ - take B = Owned(virt); - // assert (B == the_value); - return B; -} +// predicate (u8) NewByteV (pointer virt) +// { +// take B = Owned(virt); +// // assert (B == the_value); +// return B; +// } predicate void Page (pointer vbase, boolean guard, u8 order) { @@ -330,7 +330,7 @@ predicate void ZeroPage (pointer vbase, boolean guard, u8 order) let vbaseI = ((u64) vbase); // FULM_OPT take Bytes = each (u64 i; (vbaseI <= i) && (i < (vbaseI + length))) - {NewByteV(array_shift(NULL, i))}; + {RW(array_shift(NULL, i))}; assert (each (u64 i; (vbaseI <= i) && (i < (vbaseI + length))) {Bytes[i] == 0u8}); return; @@ -344,7 +344,7 @@ predicate void AllocatorPageZeroPart (pointer zero_start, u8 order) let length = region_length - sizeof; // FULM_OPT take Bytes = each (u64 i; (start <= i) && (i < (start + length))) - {NewByteV(array_shift(NULL, i))}; + {RW(array_shift(NULL, i))}; assert (each (u64 i; (start <= i) && (i < (start + length))) {Bytes[i] == 0u8}); return; From 20f72a72dfc059388d43634667c891c9f2288f40 Mon Sep 17 00:00:00 2001 From: Rini Banerjee Date: Tue, 24 Mar 2026 00:57:04 +0000 Subject: [PATCH 4/4] Change call to Byte to Block primitive --- defs.h | 2 +- run.sh | 5 ++++- 2 files changed, 5 insertions(+), 2 deletions(-) diff --git a/defs.h b/defs.h index a78a2a3..0675af1 100644 --- a/defs.h +++ b/defs.h @@ -315,7 +315,7 @@ predicate void Page (pointer vbase, boolean guard, u8 order) let vbaseI = (u64) vbase; // FULM_OPT take Bytes = each (u64 i; (vbaseI <= i) && (i < (vbaseI + length))) - {Byte(array_shift(NULL, i))}; + {Block(array_shift(NULL, i))}; return; } } diff --git a/run.sh b/run.sh index 4b122e1..dbc3efd 100755 --- a/run.sh +++ b/run.sh @@ -10,5 +10,8 @@ $CC -g -c -O0 -std=gnu11 -I$OPAM_SWITCH_PREFIX/lib/cn/runtime/include build/driv echo "Linking..." $CC driver.pp.exec.o $OPAM_SWITCH_PREFIX/lib/cn/runtime/libcn_exec.a -L $OPAM_SWITCH_PREFIX/lib/cn/runtime -lcn_exec -o driver.exe echo "Running..." -./driver.exe +for i in $(seq 1 10); +do + gtime -f ~%e~%M ./driver.exe +done echo "Done!"