[PATCH 10/18] adds weak memory models
Andrew.Butterfield at scss.tcd.ie
Andrew.Butterfield at scss.tcd.ie
Thu Dec 22 11:42:20 UTC 2022
---
.../models/threadq/Weak-Memory/RAM.pml | 48 +++++
.../models/threadq/Weak-Memory/SPARC-TSO.pml | 198 ++++++++++++++++++
.../threadq/Weak-Memory/memory_model.pml | 60 ++++++
.../models/threadq/Weak-Memory/wmemory.pml | 74 +++++++
4 files changed, 380 insertions(+)
create mode 100644 formal/promela/models/threadq/Weak-Memory/RAM.pml
create mode 100644 formal/promela/models/threadq/Weak-Memory/SPARC-TSO.pml
create mode 100644 formal/promela/models/threadq/Weak-Memory/memory_model.pml
create mode 100644 formal/promela/models/threadq/Weak-Memory/wmemory.pml
diff --git a/formal/promela/models/threadq/Weak-Memory/RAM.pml b/formal/promela/models/threadq/Weak-Memory/RAM.pml
new file mode 100644
index 00000000..70851917
--- /dev/null
+++ b/formal/promela/models/threadq/Weak-Memory/RAM.pml
@@ -0,0 +1,48 @@
+/* SPDX-License-Identifier: BSD-2-Clause */
+
+/******************************************************************************
+ * RAM
+ *
+ * Copyright (C) 2021 Trinity College Dublin (www.tcd.ie)
+ *
+ * All rights reserved.
+ *
+ * Redistribution and use in source and binary forms, with or without
+ * modification, are permitted provided that the following conditions are
+ * met:
+ *
+ * * Redistributions of source code must retain the above copyright
+ * notice, this list of conditions and the following disclaimer.
+ *
+ * * Redistributions in binary form must reproduce the above
+ * copyright notice, this list of conditions and the following
+ * disclaimer in the documentation and/or other materials provided
+ * with the distribution.
+ *
+ * * Neither the name of the copyright holders nor the names of its
+ * contributors may be used to endorse or promote products derived
+ * from this software without specific prior written permission.
+ *
+ * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+ * "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+ * LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+ * A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
+ * OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
+ * SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
+ * LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
+ * DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
+ * THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
+ * (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
+ * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ ******************************************************************************/
+
+#ifndef _FORMAL_MEMORY_RAM
+#define _FORMAL_MEMORY_RAM
+
+
+// We assume a byte-memory
+#define MEM_SIZE 8
+byte memory[MEM_SIZE] ;
+
+
+#endif
diff --git a/formal/promela/models/threadq/Weak-Memory/SPARC-TSO.pml b/formal/promela/models/threadq/Weak-Memory/SPARC-TSO.pml
new file mode 100644
index 00000000..d47e1284
--- /dev/null
+++ b/formal/promela/models/threadq/Weak-Memory/SPARC-TSO.pml
@@ -0,0 +1,198 @@
+/* SPDX-License-Identifier: BSD-2-Clause */
+
+/******************************************************************************
+ * SPARC-TSO.pml
+ *
+ * Copyright (C) 2021 Trinity College Dublin (www.tcd.ie)
+ *
+ * All rights reserved.
+ *
+ * Redistribution and use in source and binary forms, with or without
+ * modification, are permitted provided that the following conditions are
+ * met:
+ *
+ * * Redistributions of source code must retain the above copyright
+ * notice, this list of conditions and the following disclaimer.
+ *
+ * * Redistributions in binary form must reproduce the above
+ * copyright notice, this list of conditions and the following
+ * disclaimer in the documentation and/or other materials provided
+ * with the distribution.
+ *
+ * * Neither the name of the copyright holders nor the names of its
+ * contributors may be used to endorse or promote products derived
+ * from this software without specific prior written permission.
+ *
+ * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+ * "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+ * LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+ * A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
+ * OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
+ * SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
+ * LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
+ * DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
+ * THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
+ * (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
+ * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ ******************************************************************************/
+
+#ifndef _FORMAL_SPARC_TSO
+#define _FORMAL_SPARC_TSO
+
+
+// We assume a byte-memory
+#define MEM_SIZE 8
+byte memory[MEM_SIZE] ; // Global shared memory
+
+// Instructions: Load, Store, Atomic-Load-Store
+mtype = { LD // addr,reg reg:=mem[addr]
+ , ST // reg,addr mem[addr]:=reg
+ , SWAP // addr,reg reg,mem[addr]:=mem[addr],reg
+ , LDSTUB // addr,reg reg:=mem[addr]; mem[addr]:=0xFF
+ , WORK // ? ? Some internal work
+ , HALT // end of program (NOP, incl. pc!)
+ }
+
+typedef Instruction{
+ mtype op
+; byte addr
+; byte reg
+} ;
+
+inline load(i, a, r){
+ i.op = LD;
+ i.addr = a ;
+ i.reg = r ;
+} ;
+inline store(i, r, a) { i.op = ST; i.addr = a ; i.reg = r } ;
+inline swap(i, a, r) { i.op = SWAP; i.addr = a ; i.reg = r } ;
+inline ldstub(i, a, r) { i.op = LDSTUB; i.addr = a ; i.reg = r } ;
+
+
+
+#define REG_NUM 4
+#define CODE_SIZE 8
+typedef Processor {
+ byte regs[REG_NUM] // Processor registers
+; byte pc // Program counter
+ // FIFO write buffer of length 1
+; bool mt // True if wbuf is empty
+; byte wbufaddr // write address
+; byte wbufdata // write data
+; Instruction program[CODE_SIZE]
+} ;
+
+#define CORE_NUM 4
+Processor procs[CORE_NUM];
+
+inline execute(p) {
+ // NEED TO MOVE ALL 'LOCAL' VARS HERE INTO PROCESSOR struct
+ { byte ppc; // local copy of program counter
+ Instruction ir; // Instruction Register
+ byte tmp;
+
+ ppc = procs[p].pc;
+ ir.op = procs[p].program[ppc].op;
+ ir.addr = procs[p].program[ppc].addr;
+ ir.reg = procs[p].program[ppc].reg;
+ printf("Proc[%d]@[%d] : ",p,ppc);
+ printm(ir.op);
+ printf(" %d %d\n",ir.addr,ir.reg);
+ // Increment PC (if not HALT)
+ if
+ :: ir.op == HALT -> procs[p].pc = CODE_SIZE;
+ :: else -> procs[p].pc = ppc+1;
+ fi
+ // Perform Instruction
+ if
+ :: ir.op == LD ->
+ if
+ :: !procs[p].mt && ir.addr == procs[p].wbufaddr ->
+ procs[p].regs[ir.reg] = procs[p].wbufdata
+ printf("LD_%d from write buffer\n",p)
+ :: else ->
+ procs[p].regs[ir.reg] = memory[ir.addr];
+ printf("LD_%d from %d\n",p,ir.addr)
+ fi
+ :: ir.op == ST ->
+ procs[p].mt ; // wait for write buffer to be written out
+ procs[p].wbufaddr = ir.addr ;
+ procs[p].wbufdata = procs[p].regs[ir.reg] ;
+ procs[p].mt = false;
+ :: ir.op == SWAP ->
+ procs[p].mt ; // wait for write buffer to be written out
+ atomic{
+ tmp = memory[ir.addr];
+ printf("LD_%d from %d\n",p,ir.addr);
+ memory[ir.addr] = procs[p].regs[ir.reg];
+ printf("ST_%d to %d\n",p,ir.addr);
+ }
+ procs[p].regs[ir.reg] = tmp;
+ :: ir.op == LDSTUB ->
+ procs[p].mt ;
+ atomic{
+ procs[p].regs[ir.reg] = memory[ir.addr];
+ printf("LD_%d from %d\n",p,ir.addr);
+ memory[ir.addr] = 255;
+ printf("ST_%d to %d\n",p,ir.addr);
+ }
+ :: else // WORK, HALT
+ fi
+ }
+}
+
+inline runproc(p) {
+ do
+ :: procs[p].pc == CODE_SIZE -> break;
+ :: else -> execute(p);
+ od
+}
+
+inline writer(p) {
+ do
+ :: !procs[p].mt ->
+ memory[procs[p].wbufaddr] = procs[p].wbufdata;
+ printf("ST_%d from write buffer to %d\n",p,procs[p].wbufaddr);
+ procs[p].mt -> true;
+ od
+}
+
+proctype Runner(byte p) {
+ runproc(p);
+}
+
+proctype Writer(byte p) {
+ writer(p);
+}
+
+init {
+ int i;
+
+ printf("Booting up...\n");
+ do
+ :: i == CORE_NUM -> break ;
+ :: else ->
+ procs[i].pc = 0;
+ procs[i].mt = true;
+ store(procs[i].program[0],1,1);
+ load(procs[i].program[1],1,1);
+ store(procs[i].program[2],1,1);
+ swap(procs[i].program[3],1,1);
+ store(procs[i].program[4],1,1);
+ ldstub(procs[i].program[5],1,1);
+ store(procs[i].program[6],1,1);
+ i++;
+ od
+
+ printf("Running...\n");
+ atomic{
+ run Writer(0); run Runner(0);
+ run Writer(1); run Runner(1);
+ run Writer(2); run Runner(2);
+ run Writer(3); run Runner(3);
+ }
+
+
+}
+
+#endif
diff --git a/formal/promela/models/threadq/Weak-Memory/memory_model.pml b/formal/promela/models/threadq/Weak-Memory/memory_model.pml
new file mode 100644
index 00000000..14a259cb
--- /dev/null
+++ b/formal/promela/models/threadq/Weak-Memory/memory_model.pml
@@ -0,0 +1,60 @@
+/* SPDX-License-Identifier: BSD-2-Clause */
+
+/******************************************************************************
+ * memory_model
+ *
+ * Copyright (C) 2019-2021 Trinity College Dublin (www.tcd.ie)
+ *
+ * All rights reserved.
+ *
+ * Redistribution and use in source and binary forms, with or without
+ * modification, are permitted provided that the following conditions are
+ * met:
+ *
+ * * Redistributions of source code must retain the above copyright
+ * notice, this list of conditions and the following disclaimer.
+ *
+ * * Redistributions in binary form must reproduce the above
+ * copyright notice, this list of conditions and the following
+ * disclaimer in the documentation and/or other materials provided
+ * with the distribution.
+ *
+ * * Neither the name of the copyright holders nor the names of its
+ * contributors may be used to endorse or promote products derived
+ * from this software without specific prior written permission.
+ *
+ * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+ * "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+ * LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+ * A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
+ * OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
+ * SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
+ * LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
+ * DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
+ * THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
+ * (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
+ * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ ******************************************************************************/
+
+#include "RAM.pml"
+
+#include "wmemory.pml"
+
+init {
+ int nr_pr;
+
+ printf("\n\n Memory Model running.\n");
+
+ nr_pr = _nr_pr;
+
+ run WeakIncrement(0);
+ run WeakIncrement(0);
+
+ nr_pr == _nr_pr;
+
+ printf("memory[0] is %d\n", memory[0]);
+
+ assert( memory[0] == 2 );
+
+ printf("\nMemory Model finished !\n\n")
+}
diff --git a/formal/promela/models/threadq/Weak-Memory/wmemory.pml b/formal/promela/models/threadq/Weak-Memory/wmemory.pml
new file mode 100644
index 00000000..8fcff0f7
--- /dev/null
+++ b/formal/promela/models/threadq/Weak-Memory/wmemory.pml
@@ -0,0 +1,74 @@
+/* SPDX-License-Identifier: BSD-2-Clause */
+
+/******************************************************************************
+ * wmemory
+ *
+ * Copyright (C) 2019-2021 Trinity College Dublin (www.tcd.ie)
+ *
+ * All rights reserved.
+ *
+ * Redistribution and use in source and binary forms, with or without
+ * modification, are permitted provided that the following conditions are
+ * met:
+ *
+ * * Redistributions of source code must retain the above copyright
+ * notice, this list of conditions and the following disclaimer.
+ *
+ * * Redistributions in binary form must reproduce the above
+ * copyright notice, this list of conditions and the following
+ * disclaimer in the documentation and/or other materials provided
+ * with the distribution.
+ *
+ * * Neither the name of the copyright holders nor the names of its
+ * contributors may be used to endorse or promote products derived
+ * from this software without specific prior written permission.
+ *
+ * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+ * "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+ * LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+ * A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
+ * OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
+ * SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
+ * LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
+ * DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
+ * THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
+ * (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
+ * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ ******************************************************************************/
+
+#ifndef _FORMAL_WEAK_MEMORY
+#define _FORMAL_WEAK_MEMORY
+
+#include "RAM.pml"
+
+// What memory access really looks like:
+
+inline weak_load (register, address, aether)
+{
+ aether = memory[address] ;
+ register = aether
+}
+
+inline weak_store (register, address, aether)
+{
+ aether = register ;
+ memory[address] = aether
+}
+
+// Simple scenario: two processes interleave an increment.
+inline weak_increment (register, address, aether)
+{
+ weak_load(register, address, aether);
+ register++;
+ weak_store(register, address, aether)
+}
+
+proctype WeakIncrement(byte addr)
+{
+ byte reg,ethr;
+
+ weak_increment(reg,addr,ethr)
+}
+
+
+#endif
--
2.37.1 (Apple Git-137.1)
More information about the devel
mailing list