# Modelling Example - Shared Memory¶

How can we model shared memory, i.e., a global variable, in [TorXakis][7]? For simplicity, we will assume that the shared memory stores a value of Data Type Int.

## Basic Solution¶

We define a process memory to manage the shared memory. In the basic solution, this memory process has two communication channels of Data Type Int: Read and Write. This memory process is a recursive process, with one parameter: the current memory value. The process

• either provides the current value over the Read channel,

• or receives a new value over the Write channel. Since reading a value from memory doesn’t change its value, after reading, the memory process is instantiated with the current memory value. Since writing a value to memory changes its value, after writing, the memory process is instantiated with the new value.

PROCDEF memory [ Read, Write :: Int ] ( value :: Int ) ::=
##
Write ? newValue  >->  memory [Read, Write]( newValue )
ENDDEF


The memory process is used as follows, with initial value 0:

PROCDEF usage [ Read, Write :: Int ] ( ) ::=
memory [ Read, Write ] ( 0 )
someProcesses [ Read, Write ] ()
ENDDEF


where someProcesses contains read statements like

Statement

Action

Read ? x

Read ! 0

Read the memory when the value is zero

Read ? x [[ x < 0 ]]

Read the memory when the value is less then zero

and write statements like

Statement

Action

Write ! 123

Write 123 to memory

Write ? x

Write an arbritrary value to memory

Write ? x [[ x > 123 ]]

Write a value larger than 123 to memory

See the example ReadWriteConflict for more details.

In the advanced solution, the memory process has only one communication channel: Memory. This communication channel has as Data Type MemoryAccess which is defined as follows

TYPEDEF MemoryAccess ::= Read  { value :: Int }
| Write { newValue :: Int }
ENDDEF


The memory process is still a recursive process, with one parameter: the current memory value. The process

• either provides the Read constructor with the current value over the Memory channel,

• or receives a Write constructor with the new value over the Memory channel. Since reading a value from memory doesn’t change its value, after reading, the memory process is instantiated with the current memory value. Since writing a value to memory changes its value, after writing, the memory process is instantiated with the new value.

PROCDEF memory [ Memory :: MemoryAccess ] ( value :: Int ) ::=
Memory ! Read ( value )     >->  memory [Memory](value)
##
Memory ? x [[ isWrite(x) ]] >->  memory [Memory](newValue(x))
ENDDEF


The memory process is used as follows, with initial value 0:

PROCDEF usage [ Memory :: MemoryAccess ] ( ) ::=
memory [ Memory ] ( 0 )
|[ Memory ]|
someProcesses [ Memory ] ()
ENDDEF


where someProcesses contains read statements like

Statement

Action

Memory ? x [[ isRead(x) ]]

Memory ! Read(0)

Read the memory when the value is zero

Memory ? x [[ isRead(x) /\ (value(x) < 0) ]]

Read the memory when the value is less then zero

and write statements like

Statement

Action

Memory ! Write(123)

Write 123 to memory

Memory ? x [[ isWrite(x) ]]

Write an arbritrary value to memory

Memory ? x [[ isWrite(x) /\ (newValue(x) > 123) ]]

Write a value larger than 123 to memory

## Using Test Purposes¶

In order to be able to use Test Purposes for this case, we need to be able to identify end states. If we add a way to identify who accesses a memory cell at a certain point, then we can also use it to signal an end state. Let’s define MemoryAccess and the cell that is accessed separately:

TYPEDEF MemoryAccess ::= MemoryAccess { identity :: String; value :: Int }
ENDDEF

PROCDEF cell [ Read, Write :: MemoryAccess ] ( value :: Int ) ::=
Read ? ma [[ value (ma) == value]] >-> cell [Read, Write ] (value)
##
Write ? ma >->  cell [Read, Write] (value (ma))
ENDDEF


The cell process is used as follows, with initial value 0:

PROCDEF usage [ Read, Write :: MemoryAccess ] ( ) ::=
cell [ Read, Write ] ( 0 )
someProcess[ Read, Write ] ( )
ENDDEF


where someProcesses is similar to ones in previous examples but also contains read statements that signals end states:

Statement

Action

Read ? ma [[ identity (ma) == "Final"]]

Read the value in memory by a process that is identified as “Final”

Let’s create a Model for this usage:

CHANDEF Channels ::=
ENDDEF

MODELDEF Model ::=
CHAN IN Dummy

BEHAVIOUR
system [ Read, Write ] ( )
ENDDEF

CNECTDEF  Sut ::=
CLIENTSOCK

CHAN OUT Dummy                   HOST "localhost"  PORT 7776
ENCODE   Dummy ? s               -> ! toString(s)
CHAN IN  Read                    HOST "localhost"  PORT 7777
DECODE   Read ! fromString(s)    <- ? s
CHAN IN  Write                   HOST "localhost"  PORT 7778
DECODE   Write ! fromString(s)   <- ? s
ENDDEF

CNECTDEF  Sim ::=
SERVERSOCK

CHAN IN   Dummy                   HOST "localhost"  PORT 7776
DECODE    Dummy ! fromString(s)   <- ? s
CHAN OUT  Read                    HOST "localhost"  PORT 7777
ENCODE    Read ? b                ->  ! toString(b)
CHAN OUT  Write                   HOST "localhost"  PORT 7778
ENCODE    Write ? b               ->  ! toString(b)
ENDDEF


Both Read and Write channels are output channels but we also need a simulator in order to run Test Purposes, and simulator needs an input channel in order to run properly. Hence, the Dummy channel.

Now we can write a Test Purpose that manipulates the inputs and observes the outputs:

PROCDEF output [Read, Write :: MemoryAccess](n :: Int) HIT ::=
Read ! MemoryAccess ("Final",n) >-> HIT
##
Read ? ma [[ (identity(ma) <> "Final") \/ (value(ma) <> n)]] >-> output [Read, Write](n)
##
Write ? ma >-> output [Read, Write](n)
ENDDEF

PURPDEF TestPurpose ::=
CHAN IN   Dummy

This Test Purpose will run until someProcess process in the usage performs Read accesses with “Final” identity and each of the given values (1,2 and 3), or given number of steps are performed by TorXakis.