[rtems-central commit] Chains API model and test gen material
Sebastian Huber
sebh at rtems.org
Wed Jan 18 11:35:17 UTC 2023
Module: rtems-central
Branch: master
Commit: 87c48b30ca1c818df467bb3fbcab67046888050e
Changeset: http://git.rtems.org/rtems-central/commit/?id=87c48b30ca1c818df467bb3fbcab67046888050e
Author: Andrew Butterfield <Andrew.Butterfield at scss.tcd.ie>
Date: Tue Jan 10 19:47:09 2023 +0000
Chains API model and test gen material
---
formal/promela/models/chains/.gitignore | 1 +
.../promela/models/chains/chains-api-model-post.h | 3 +
.../promela/models/chains/chains-api-model-pre.h | 43 +++++
.../promela/models/chains/chains-api-model-rfn.yml | 64 +++++++
.../promela/models/chains/chains-api-model-run.h | 18 ++
formal/promela/models/chains/chains-api-model.pml | 203 +++++++++++++++++++++
formal/promela/models/chains/tr-chains-api-model.c | 70 +++++++
formal/promela/models/chains/tr-chains-api-model.h | 57 ++++++
8 files changed, 459 insertions(+)
diff --git a/formal/promela/models/chains/.gitignore b/formal/promela/models/chains/.gitignore
new file mode 100644
index 00000000..daa24295
--- /dev/null
+++ b/formal/promela/models/chains/.gitignore
@@ -0,0 +1 @@
+tr-model-chains-api-*.c
diff --git a/formal/promela/models/chains/chains-api-model-post.h b/formal/promela/models/chains/chains-api-model-post.h
new file mode 100644
index 00000000..d826725d
--- /dev/null
+++ b/formal/promela/models/chains/chains-api-model-post.h
@@ -0,0 +1,3 @@
+/* SPDX-License-Identifier: BSD-2-Clause */
+
+/* post-amble empty for now */
diff --git a/formal/promela/models/chains/chains-api-model-pre.h b/formal/promela/models/chains/chains-api-model-pre.h
new file mode 100644
index 00000000..9816a5ad
--- /dev/null
+++ b/formal/promela/models/chains/chains-api-model-pre.h
@@ -0,0 +1,43 @@
+/* SPDX-License-Identifier: BSD-2-Clause */
+
+/******************************************************************************
+ * Chains API 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 <rtems.h>
+#include <rtems/test.h>
+#include <rtems/chain.h>
+#include "tr-chains-api-model.h"
diff --git a/formal/promela/models/chains/chains-api-model-rfn.yml b/formal/promela/models/chains/chains-api-model-rfn.yml
new file mode 100644
index 00000000..103e32ce
--- /dev/null
+++ b/formal/promela/models/chains/chains-api-model-rfn.yml
@@ -0,0 +1,64 @@
+# SPDX-License-Identifier: BSD-2-Clause
+# Event Manager: Promela to RTEMS Refinement
+
+# Copyright (C) 2019-2021 Trinity College Dublin (www.tcd.ie)
+#
+# Redistribution and use in source and binary forms, with or without
+# modification, are permitted provided that the following conditions
+# are met:
+# 1. Redistributions of source code must retain the above copyright
+# notice, this list of conditions and the following disclaimer.
+# 2. 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.
+#
+# 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.
+
+NAME: |
+ const char rtems_test_name[] = "Model_Chain_API";
+
+memory_DCL: item {0}[{1}];
+
+nptr_DCL: item *
+
+chain_DCL: rtems_chain_control
+
+INIT: rtems_chain_initialize_empty( &chain );
+
+append: |
+ memory[{1}].val = {0};
+ rtems_chain_append_unprotected( &chain, (rtems_chain_node*)&memory[{1}] );
+
+getNonNull: |
+ nptr = get_item( &chain );
+ T_eq_ptr( nptr, &memory[{0}] );
+
+nptr: T_eq_ptr( nptr, &memory[{0}] );
+
+nptr_PTR: |
+ T_eq_ptr( nptr, NULL );
+ T_eq_ptr( nptr, &memory[{0}] );
+
+itm_FSCALAR: T_eq_int( {0}->val, {1} );
+
+nxt_FPTR: |
+ T_eq_ptr( {0}->node.next->next, NULL );
+ T_eq_ptr( {0}->node.next, &memory[{1}] );
+
+prv_FPTR: |
+ T_eq_ptr( {0}->node.previous->previous, NULL );
+ T_eq_ptr( {0}->node.previous, &memory[{1}] );
+
+chain_SEQ: |
+ show_chain( &chain, ctx->buffer );
+ T_eq_str( ctx->buffer, "{0} 0" );
diff --git a/formal/promela/models/chains/chains-api-model-run.h b/formal/promela/models/chains/chains-api-model-run.h
new file mode 100644
index 00000000..292718ee
--- /dev/null
+++ b/formal/promela/models/chains/chains-api-model-run.h
@@ -0,0 +1,18 @@
+/* SPDX-License-Identifier: BSD-2-Clause */
+
+void RtemsModelChainsAPI_Run{0}(
+)
+{{
+ Context ctx;
+
+ memset( &ctx, 0, sizeof( ctx ) );
+
+ T_set_verbosity( T_NORMAL );
+
+ TestSegment0( &ctx );
+}}
+
+T_TEST_CASE( RtemsModelChainAPI{0} )
+{{
+ RtemsModelChainsAPI_Run{0}( );
+}}
diff --git a/formal/promela/models/chains/chains-api-model.pml b/formal/promela/models/chains/chains-api-model.pml
new file mode 100644
index 00000000..b76a8628
--- /dev/null
+++ b/formal/promela/models/chains/chains-api-model.pml
@@ -0,0 +1,203 @@
+/* SPDX-License-Identifier: BSD-2-Clause */
+
+/******************************************************************************
+ * chains-api-model.pml
+ *
+ * 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.
+ ******************************************************************************/
+
+// Sizings, MEM_SIZE = 2 ** PTR_SIZE
+#define PTR_SIZE 3
+#define MEM_SIZE 8
+
+// Nodes types
+typedef Node {
+ unsigned nxt : PTR_SIZE
+; unsigned prv : PTR_SIZE
+; byte itm
+}
+
+inline ncopy (dst,src) {
+ dst.nxt = src.nxt; dst.prv=src.prv; dst.itm = src.itm
+}
+
+// Memory
+Node memory[MEM_SIZE] ;
+unsigned nptr : PTR_SIZE ; // one node pointer
+
+// We ignore pointer values here as their values depend on $RTEMS_DEBUG
+inline show_node (){
+ atomic{
+ printf("@@@ 0 PTR nptr %d\n",nptr);
+ if
+ :: nptr -> printf("@@@ 0 STRUCT nptr\n");
+ // printf("@@@ 0 PTR nxt %d\n", memory[nptr].nxt);
+ // printf("@@@ 0 PTR prv %d\n", memory[nptr].prv);
+ printf("@@@ 0 SCALAR itm %d\n", memory[nptr].itm);
+ printf("@@@ 0 END nptr\n")
+ :: else -> skip
+ fi
+ }
+}
+
+typedef Control {
+ unsigned head : PTR_SIZE
+; unsigned tail : PTR_SIZE
+; unsigned size : PTR_SIZE
+}
+
+Control chain ; // one chain
+
+
+inline show_chain () {
+ int cnp;
+ atomic{
+ cnp = chain.head;
+ printf("@@@ 0 SEQ chain\n");
+ do
+ :: (cnp == 0) -> break;
+ :: (cnp != 0) ->
+ printf("@@@ 0 SCALAR _ %d\n",memory[cnp].itm);
+ cnp = memory[cnp].nxt
+ od
+ printf("@@@ 0 END chain\n");
+ }
+}
+
+inline append(ch,np) {
+ assert(np!=0);
+ assert(ch.size < 7);
+ if
+ :: (ch.head == 0) ->
+ ch.head = np;
+ ch.tail = np;
+ ch.size = 1;
+ memory[np].nxt = 0;
+ memory[np].prv = 0;
+ :: (ch.head != 0) ->
+ memory[ch.tail].nxt = np;
+ memory[np].prv = ch.tail;
+ ch.tail = np;
+ ch.size = ch.size + 1;
+ fi
+}
+
+proctype doAppend(int addr; int val) {
+ atomic{
+ memory[addr].itm = val;
+ append(chain,addr);
+ printf("@@@ 0 CALL append %d %d\n",val,addr);
+ show_chain();
+ } ;
+}
+
+/* np = get(ch) */
+inline get(ch,np) {
+ np = ch.head ;
+ if
+ :: (np != 0) ->
+ ch.head = memory[np].nxt;
+ ch.size = ch.size - 1;
+ // memory[np].nxt = 0
+ :: (np == 0) -> skip
+ fi
+ if
+ :: (ch.head == 0) -> ch.tail = 0
+ :: (ch.head != 0) -> skip
+ fi
+}
+
+proctype doGet() {
+ atomic{
+ get(chain,nptr);
+ printf("@@@ 0 CALL get %d\n",nptr);
+ show_chain();
+ assert(nptr != 0);
+ show_node();
+ } ;
+}
+
+/* -----------------------------
+ doNonNullGet waits for a non-empty chain
+ before doing a get.
+ In generated sequential C code this can be simply be treated
+ the same as a call to doGet()
+*/
+proctype doNonNullGet() {
+ atomic{
+ chain.head != 0;
+ get(chain,nptr);
+ printf("@@@ 0 CALL getNonNull %d\n",nptr);
+ show_chain();
+ assert(nptr != 0);
+ show_node();
+ } ;
+}
+
+
+init {
+ pid nr;
+ atomic{
+ printf("\n\n Chain Model running.\n");
+ printf("@@@ 0 NAME Chain_AutoGen\n")
+ printf("@@@ 0 DEF MAX_SIZE 8\n");
+ printf("@@@ 0 DCLARRAY Node memory MAX_SIZE\n");
+ printf("@@@ 0 DECL unsigned nptr NULL\n")
+ printf("@@@ 0 DECL Control chain\n");
+
+ printf("\nInitialising...\n")
+ printf("@@@ 0 INIT\n");
+ chain.head = 0; chain.tail = 0; chain.size = 0;
+ show_chain();
+ show_node();
+ } ;
+
+ nr = _nr_pr;
+
+ run doAppend(6,21);
+ run doAppend(3,22);
+ run doAppend(4,23);
+ run doNonNullGet();
+ run doNonNullGet();
+ run doNonNullGet();
+
+ nr == _nr_pr;
+
+#ifdef TEST_GEN
+ assert (chain.size != 0);
+#else
+ assert (chain.size == 0);
+#endif
+
+ printf("\nChain Model finished !\n\n")
+}
diff --git a/formal/promela/models/chains/tr-chains-api-model.c b/formal/promela/models/chains/tr-chains-api-model.c
new file mode 100644
index 00000000..05938362
--- /dev/null
+++ b/formal/promela/models/chains/tr-chains-api-model.c
@@ -0,0 +1,70 @@
+/* SPDX-License-Identifier: BSD-2-Clause */
+
+/******************************************************************************
+ * Chains API 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 <rtems.h>
+#include <rtems/test.h>
+#include <rtems/chain.h>
+#include "tr-chains-api-model.h"
+
+item* get_item( rtems_chain_control* control )
+{
+ return (item*) rtems_chain_get_unprotected( control );
+}
+
+void show_chain( rtems_chain_control *control, char *str )
+{
+ item *itm;
+ rtems_chain_node *nod;
+ int cp, len;
+ char *s;
+
+ nod = (rtems_chain_node *)&control->Head;
+ itm = (item *)nod->next;
+ // itm is not NULL
+ s = str;
+ len = BUFSIZE;
+ while ( (item*)((rtems_chain_node*)itm)->next ) { // NULL when at control
+ cp = T_snprintf( s, len, " %d",itm->val );
+ s += cp;
+ len -= cp;
+ itm = (item*)((rtems_chain_node*)itm)->next;
+ }
+ cp = T_snprintf( s, len, " 0" );
+ s += cp;
+ len -= cp;
+}
diff --git a/formal/promela/models/chains/tr-chains-api-model.h b/formal/promela/models/chains/tr-chains-api-model.h
new file mode 100644
index 00000000..18c2c9b6
--- /dev/null
+++ b/formal/promela/models/chains/tr-chains-api-model.h
@@ -0,0 +1,57 @@
+/* SPDX-License-Identifier: BSD-2-Clause */
+
+/******************************************************************************
+ * Chains API 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.
+ ******************************************************************************/
+
+
+typedef struct item
+{
+ rtems_chain_node node;
+ int val;
+} item;
+
+item* get_item( rtems_chain_control* control);
+
+void show_chain(rtems_chain_control *control, char *str);
+
+#define BUFSIZE 80
+
+typedef struct {
+ int stuff;
+ char buffer[BUFSIZE];
+} RtemsModelChainsAPI_Context;
+
+typedef RtemsModelChainsAPI_Context Context;
More information about the vc
mailing list