source: rtems-central/formal/promela/models/chains/chains-api-model.pml @ 87c48b3

Last change on this file since 87c48b3 was 87c48b3, checked in by Andrew Butterfield <Andrew.Butterfield@…>, on 01/10/23 at 19:47:09

Chains API model and test gen material

  • Property mode set to 100644
File size: 5.2 KB
Line 
1/* SPDX-License-Identifier: BSD-2-Clause */
2
3/******************************************************************************
4 * chains-api-model.pml
5 *
6 * Copyright (C) 2019-2021 Trinity College Dublin (www.tcd.ie)
7 *
8 * All rights reserved.
9 *
10 * Redistribution and use in source and binary forms, with or without
11 * modification, are permitted provided that the following conditions are
12 * met:
13 *
14 *     * Redistributions of source code must retain the above copyright
15 *       notice, this list of conditions and the following disclaimer.
16 *
17 *     * Redistributions in binary form must reproduce the above
18 *       copyright notice, this list of conditions and the following
19 *       disclaimer in the documentation and/or other materials provided
20 *       with the distribution.
21 *
22 *     * Neither the name of the copyright holders nor the names of its
23 *       contributors may be used to endorse or promote products derived
24 *       from this software without specific prior written permission.
25 *
26 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
27 * "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
28 * LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
29 * A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
30 * OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
31 * SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
32 * LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
33 * DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
34 * THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
35 * (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
36 * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
37 ******************************************************************************/
38
39// Sizings, MEM_SIZE = 2 ** PTR_SIZE
40#define PTR_SIZE 3
41#define MEM_SIZE 8
42
43// Nodes types
44typedef Node {
45  unsigned nxt  : PTR_SIZE
46; unsigned prv  : PTR_SIZE
47; byte     itm
48}
49
50inline ncopy (dst,src) {
51  dst.nxt = src.nxt; dst.prv=src.prv; dst.itm = src.itm
52}
53
54// Memory
55Node memory[MEM_SIZE] ;
56unsigned nptr : PTR_SIZE ;  // one node pointer
57
58// We ignore pointer values here as their values depend on $RTEMS_DEBUG
59inline show_node (){
60   atomic{
61     printf("@@@ 0 PTR nptr %d\n",nptr);
62     if
63     :: nptr -> printf("@@@ 0 STRUCT nptr\n");
64                // printf("@@@ 0 PTR nxt %d\n", memory[nptr].nxt);
65                // printf("@@@ 0 PTR prv %d\n", memory[nptr].prv);
66                printf("@@@ 0 SCALAR itm %d\n", memory[nptr].itm);
67                printf("@@@ 0 END nptr\n")
68     :: else -> skip
69     fi
70   }
71}
72
73typedef Control {
74  unsigned head : PTR_SIZE
75; unsigned tail : PTR_SIZE
76; unsigned size : PTR_SIZE
77}
78
79Control chain ; // one chain
80
81
82inline show_chain () {
83   int cnp;
84   atomic{
85     cnp = chain.head;
86     printf("@@@ 0 SEQ chain\n");
87     do
88       :: (cnp == 0) -> break;
89       :: (cnp != 0) ->
90            printf("@@@ 0 SCALAR _ %d\n",memory[cnp].itm);
91            cnp = memory[cnp].nxt
92     od
93     printf("@@@ 0 END chain\n");
94   }
95}
96
97inline append(ch,np) {
98  assert(np!=0);
99  assert(ch.size < 7);
100  if
101    :: (ch.head == 0) ->
102         ch.head = np;
103         ch.tail = np;
104         ch.size = 1;
105         memory[np].nxt = 0;
106         memory[np].prv = 0;
107    :: (ch.head != 0) ->
108         memory[ch.tail].nxt = np;
109         memory[np].prv = ch.tail;
110         ch.tail = np;
111         ch.size = ch.size + 1;
112  fi
113}
114
115proctype doAppend(int addr; int val) {
116  atomic{
117    memory[addr].itm = val;
118    append(chain,addr);
119    printf("@@@ 0 CALL append %d %d\n",val,addr);
120    show_chain();
121  } ;
122}
123
124/* np = get(ch) */
125inline get(ch,np) {
126  np = ch.head ;
127  if
128    :: (np != 0) ->
129         ch.head = memory[np].nxt;
130         ch.size = ch.size - 1;
131         // memory[np].nxt = 0
132    :: (np == 0) -> skip
133  fi
134  if
135    :: (ch.head == 0) -> ch.tail = 0
136    :: (ch.head != 0) -> skip
137  fi
138}
139
140proctype doGet() {
141  atomic{
142    get(chain,nptr);
143    printf("@@@ 0 CALL get %d\n",nptr);
144    show_chain();
145    assert(nptr != 0);
146    show_node();
147  } ;
148}
149
150/* -----------------------------
151 doNonNullGet waits for a non-empty chain
152 before doing a get.
153 In generated sequential C code this can be simply be treated
154  the same as a call to doGet()
155*/
156proctype doNonNullGet() {
157  atomic{
158    chain.head != 0;
159    get(chain,nptr);
160    printf("@@@ 0 CALL getNonNull %d\n",nptr);
161    show_chain();
162    assert(nptr != 0);
163    show_node();
164  } ;
165}
166
167
168init {
169  pid nr;
170  atomic{
171    printf("\n\n Chain Model running.\n");
172    printf("@@@ 0 NAME Chain_AutoGen\n")
173    printf("@@@ 0 DEF MAX_SIZE 8\n");
174    printf("@@@ 0 DCLARRAY Node memory MAX_SIZE\n");
175    printf("@@@ 0 DECL unsigned nptr NULL\n")
176    printf("@@@ 0 DECL Control chain\n");
177
178    printf("\nInitialising...\n")
179    printf("@@@ 0 INIT\n");
180    chain.head = 0; chain.tail = 0; chain.size = 0;
181    show_chain();
182    show_node();
183  } ;
184
185  nr = _nr_pr;
186
187  run doAppend(6,21);
188  run doAppend(3,22);
189  run doAppend(4,23);
190  run doNonNullGet();
191  run doNonNullGet();
192  run doNonNullGet();
193
194  nr == _nr_pr;
195
196#ifdef TEST_GEN
197  assert (chain.size != 0);
198#else
199  assert (chain.size == 0);
200#endif
201
202  printf("\nChain Model finished !\n\n")
203}
Note: See TracBrowser for help on using the repository browser.