Process Algebra Language Tool

Michael D. Rice

Department of Mathematics & Computer Science
Wesleyan University
Middletown, CT 06459
mrice@wesleyan.edu
http://mrice.web.wesleyan.edu

March 5, 1999

0. Sections

1. IntroductionTop of Page

The Process Algebra Language (PAL) is an imperative programming language that permits the description of a class of concurrent programs. A PAL program is executed by translating it into a collection of tree representations. These representations are interpreted in a simulator environment based on a runtime scheduler and thread manager that uses execution and waiting lists.

The syntax and semantics of PAL is similar to that of the CSP and occam languages ([H], [O]). For example, PAL has a process-oriented syntax and processes communicate using statically specified channels. In addition, each process can be encapsulated in a procedure that can be instantiated to run the process. However, PAL differs from both languages in the following aspects.

The motivation for developing PAL was the need for a flexible software tool to specify and observe the runtime behavior of various components in the architectural description language ASDL [RS]. The use of the language in this context will be discussed in another document.

The PAL language is currently implemented in Visual Basic 4.0 and uses an Access 7.0 database to store programs and error messages.

2. SyntaxTop of Page

    program ::= {id [ ( id_list ) 1 ] = process}+

    process ::= call | cond | comp | icomp | comm | atom

    call 2 ::= CALL id [ [ intexp_list ] ]

    cond 3 ::= IF boolexp process process

    comp 4 ::= (PAR | SEQ | ALT| OR) (process { , process})

    icomp 5 ::= (ITPAR | ITSEQ | ITALT | ITOR) (id, intexp, process)

    comm 6 ::= (cname ? var | cname ! intexp | var = intexp | WAIT [ intexp ] ) & process

    atom 7 ::= SKIP | STOP

    cname ::= var
    var ::= id [ [ intexp ] ]
    id_list ::= id { , id }
    id ::= usual definition with _ allowed after the first alphabetical character
    intexp_list ::= intexp { , intexp }
    intexp ::= arithmetic expression that evaluates to an integer
    boolexp ::= boolean expression that evalutes to True or False

3. Semantics Top of Page

Overview

1

For a named process id, the members of id_list are read-only parameters of type integer.

2

The statement CALL id [..] denotes the instantiation of the named process id based on the values of the expressions in intexp_list.

3

The statement IF bool P Q denotes the standard conditional: if the boolean expression bool evaluates to True, then P will be executed; otherwise, Q will be executed. There is no loop construct, so loops must be simulated by using tail recursion.

4

The statement (SEQ | PAR | ALT | OR) (P1, ... , Pn) denotes the sequential (resp. parallel, alternating, or non-deterministic) composition of the processes P1, ... , Pn.

Each process used in an ALT composition must be guarded, that is, it must have the form

cname ? var & P.
5

The statement (ITPAR | ITSEQ | ITALT | ITOR) (k, intexp, P) specifies an iterated sequential (resp. parallel, alternating, or non-deterministic) composition of N copies of the process P, 0 < k < N, where N = value(intexp). The process P may be parameterized by k and it must be guarded if it is used in an ITALT statement.

6

The statement cname ? var & P specifies an input channel process where cname consists of a channel name c (and possibly a bracketed expression [intexp]). The process P is executed after a value for the variable var is received on the channel cname.

The statement cname ! intexp & P specifies an output channel process. The process P is executed after the value of the expression intexp is sent on the channel cname.

The statement var = intexp & P specifies a process that assigns the value of the expression intexp to the variable var and then behaves like the process P.

The statement WAIT [intexp] & P specifies a process that waits for intexp time units and then behaves like P. [If value(intexp) < 1, then the process behaves like P.]

7

The symbols SKIP and STOP denote atomic processes. The process SKIP successfully terminates without engaging in any action. The process STOP deadlocks without engaging in any action.

Channels

All channel names are global and are declared by their use in either an input process cname ? var & P or an output process cname ! intexp & P. If cname has the form c[intexp], then c denotes an array of channels; otherwise, cname denotes a single channel c.

A channel is internal if there exists two distinct processes in a program such that one process receives a value on the channel and the other process sends a value on the channel. A channel is an input (output) channel if it only receives (sends) values in each process where it is used.

A communication on an internal channel requires the synchronization of the sending and receiving processes. One process has already registered its willingness to either send or receive on the channel and the other process is currently willing to either receive or send on the channel. The communication semantics is summarized by the following reduction rule:

PAR(c ? var & P, c ! intexp & Q)

var = value(intexp) & PAR(P, Q)

First, the variable var is assigned the value of the expression intexp and then the process behaves like the parallel composition of the processes following the communications.

If c is an input channel, then the process c ? var & P will deadlock, that is, behave like the process STOP, if c has not been assigned a constant default value and has not been selected to receive a value from the user during execution. In this case, c blocks the execution of P. On the other hand, if c is an output channel, then c never blocks the execution of P in a process of the form c ! intexp & P. By assumption, the value of the expression intexp will always be sent to the environment.

Variables

Each variable is local to the named process in which it is declared. A variable x is declared by either a channel input statement or an assignment statement

In the second and fourth cases, x denotes an array variable.

In general, lexical scoping is used for variables. The scope of a variable extends from its declaration to the declaration of a variable with the same name in a parallel construct (PAR, ITPAR). In addition, the scope of each variable declared in an enclosed process of a parallel construct is restricted to that process.

For example, in each of the following processes, the name x declares exactly one variable in the symbol table of the respective sequential, assignment, and iterated constructs.

On the other hand, in each of the processes

the name x declares two different variables. In the first process, the variables are found in the symbol tables of the process and the second enclosed process. In the second process, a variable is found in each symbol table of an enclosed process.

4. Sample Programs Top of Page

Factorial Function

The program contains two named processes Main and Factorial and the latter process has one integer parameter m. Based on the reserved word CALL, at runtime an instantiation of the Factorial process is created with the value of m bound to 3. The instantiation is based on an iterated sequential construct that uses the local variable x. When k = 0, x is assigned the value 1; then the multiplications x = x * 1, x = x * 2, and x = x * 3 occur, corresponding to the values k = 1, 2, and 3 respectively, giving the final value of x = 6.

Parallel Composition (no communication)

P = PAR(SKIP, STOP, SKIP)

The program is the parallel composition of three atomic processes and is equivalent to the process STOP. When the program is run, it will deadlock with the threads corresponding to the process P and a STOP process remaining in the execution list.

Parallel Composition (communication)

Test = PAR(c ! 34 & SKIP, c ? v & SKIP)

The program is the parallel composition of two processes that communicate on the channel c. The first process outputs the value 34 on c and the second process receives the value and assigns it to the variable v. When the program is run, communication on c occurs. Then each of the two SKIP processes terminate, successfully terminating the program with an empty execution list.

External Channel Usage

Test = in ? z & out ! 3 * z & SKIP

The program Test will deadlock if the channel in is not assigned a default value and is not designated as receiving a value at runtime. Otherwise, a value for z is received on the channel in and the value 3 * z is sent to the environment on the channel out.

Pipeline

The program Main uses an array of channels c[] that connect the various processes in a pipeline. Assuming that the channel in is given a default value of 2, the values 6, 12, 24, and 48 are transmitted on the channels c[0], c[1], c[2], and c[3], respectively, and the value 48 is sent to the environment on the channel out.

Nondeterministic Choice

OrTest = OR(x = 5 & out ! x - 4 & SKIP, x = 5 & out ! x * x & SKIP)

The program OrTest will execute either the first or second enclosed process based on a random choice that is independent of the environment. Then either the value 1 or the value 25 is output on the channel out depending on which process was selected.

Deterministic Choice

Main = PAR(ch[5] ! 6 & SKIP, ITALT(k, 8, ch[k] ? x & out ! k * x & SKIP))

The second enclosed process (ITALT) represents a deterministic choice that cannot execute until the first process registers an intent to output a value on channel ch[5]. When this occurs, the second process receives the value 6 on ch[5] and then behaves like the following process, so 30 is output on the channel out. The ITALT process can receive values only on the channels ch[0], ..., ch[7]. For example, if the first process is changed to ch[8] ! 6 & SKIP, then the program will deadlock.

Wait Process

The simulator has a global time variable that is incremented based on the occurence of one of the following cases: an assignment statement, communication on a channel, or the execution of a wait process WAIT[m] & P. In the first two cases, the global time is incremented by 1. In the third case, the global time is incremented by m. All other events in a program, including the evaluation of expressions, are assumed to occur instantaneously.

For example, in the program

TimeExample = x = 2 & WAIT[4] & out ! x & SKIP

the assignment process occurs at time 0, the wait process occurs at time 1, and the channel communication event occurs at time 5.

5. Parsing Top of Page

The form Main.frm (frmMain) is the user interface for editing and parsing PAL programs. The form RunTime.frm (frmRunTime) is the user interface for executing and monitoring PAL programs. There is also an auxilliary form Display.Frm (frmDisplay) that is used to display menu information.

The module ParseCSP.Bas contains the parsing routines that generate tree representations. The module ParseExp.Bas contains the routines for parsing expressions and generating postfix representations. The module SimGeneral.Bas contains all global variable declarations and routines for creating and animating the language trademark, manipulating forms, initializing the toolbar, saving files, and displaying information based on menu choices.

The application stores the strings representing programs and parsing error messages in the respective tables CSPExpTable and CSPErrorTable in the database CSPDatabase.mdb. The application also uses a variety of custom classes and windows objects. These are listed at the end of this document.

The routine ParseCSP in the module ParseCSP.Bas parses a program and generates a tree representation for each named process using the procedure call

ParseCSP(strProgram, ...)

where the string strProgram represents the text of the program.

The list of tokens used during parsing is stored in the global variable TokenList (LexicalClass). This list is generated by calling the method

TokenList.GenerateTokenList(strProgram, ...)

in the routine ParseCSP.

The routines in ParseCSP.bas also use the procedures ParseExp and ParseBoolExp in the module to parse arithmetic and boolean expressions and the global variables stkOP (StackTokenClass) and stkPostFix (StackPostfixClass) to generate the postfix representations for these expressions.

The values of the global variables ChanList (MessageClass) and ProcList (NamedProcessesClass) are computed as a program is parsed. The variable ChanList stores a channel table that consists of a collection of ChanClass objects corresponding to the distinct channel names used in the program. The variable ProcList stores a process table that consists of a collection of ProcessClass objects corresponding to the named processes used in the program.

The auxiliary global array variable TranClosure() is also computed as the program is parsed. This variable stores the transitive closure of the context graph that is used to partially check the correctness of single channel usage.

6. Execution Top of Page

Overview

During execution, the tree representation of each named process is interpreted by a scheduler that uses an execution list ExecList (ExecClass) and a waiting list WaitList (WaitClass). Each tree representation consists of a collection of nodes and references between nodes. Each node is an object of type NodeClass that contains a reference to a specialized class object. This object corresponds to a language construct such as an assignment process or a channel communication process. A node can also contain a reference to a symbol table and a reference to space for storing the values of variables.

The execution and waiting lists contain thread objects of type ThreadClass. A thread object contains a reference to one of the nodes in a tree representation. The execution list contains all threads that are either blocked or can be scheduled for execution. The waiting list contains threads with time stamps that are waiting to be added to the execution list. An overview of the scheduling algorithm is presented in the next section.

During execution, the global variable stkEval (StackIntegerClass) is used to evaluate arithmetic and boolean expressions, the global variable threadManager (StackIntegerClass) manages the allocation of thread identifiers, and the global variables LogList and ChannelLogList of type LogClass are used to record various execution events including channel communications.

The global variable Simulation (SimulationClass) is the main simulation object. It maintains the global clock, handles user interactions with the executing program, and schedules and executes threads. The method call

Simulation.RunSimulation(strProcessName, ...)

initiates the execution of the process strProcessName.

Scheduling

The call Simulation.RunSimulation(strProcessName, ...) retrieves the tree representation of the process from the process table using the method ProcList.GetProcess, creates a thread corresponding to the root node of the tree representing the process, and adds the thread to the execution list using ExecList.InsertThread. After this initialization, a scheduling loop repeatedly attempts to select a non-blocked thread from the execution list using the method ExecList.FirstNonBlockedThreadID and run the thread using the method Simulation.ExecuteThread. The execution of threads is discussed in the next section.

The following five cases are handled by the scheduling algorithm.

  1. If the execution list and waiting list are both empty, then the program successfully terminates and the simulation stops.
  2. If the waiting list is empty and each thread in the execution list is blocked, then FirstNonBlockedThreadID returns the value 0 and the simulation stops, indicating that the program has deadlocked.
  3. If the waiting list contains a thread with a time stamp equal to the current global time, then each thread in the waiting list with this time stamp is removed and added to the execution list by WaitList.ScheduleWaitingThreads. In this case, no thread is selected for execution, but the simulation continues to run.
  4. If each thread in the execution list is blocked and the waiting list is non-empty, then the global time is reset to the value of the smallest time stamp of a thread in the waiting list. Then each thread in the waiting list with this time stamp is removed and added to the execution list. In this case, no thread is selected for execution, but the simulation continues to run.
  5. If either the waiting list is empty or the time stamp of each thread in the waiting list exceeds the current global time and the execution list contains at least one non-blocked thread, then FirstNonBlockedThreadID returns a threadID corresponding to the first non-blocked thread in the execution list. Then the corresponding thread is executed by ExecuteThread which calls a method of the form Execute*Thread based on the type of node referenced by the thread.

Threads

Each of the following methods correspond to the execution of a basic language construct.

The method executes an assignment process by evaluating the arithmetic expression associated with the node referenced by the current thread and assigning this value to the associated variable in the space allocated to the current thread. The current thread's node reference is reset to the node corresponding to the process following the assignment. The global time is incremented by one unit.

The method attempts to execute the channel communication in the node referenced by the current thread. The method ChanList.GetCommThreadID is called to determine which of the following cases holds:

If (a) holds, the method Simulation.SendMessage is called to send the message between the current thread and the communicating thread. Then the node references in these threads are reset to the nodes corresponding to the processes following the channel communications.

If (b) holds, the scheduler blocks the current thread and registers the attempted channel communication in the channel table.

If (c) holds and the process is trying to receive on the channel, there are two possible outcomes depending on choices made by the user prior to execution. If either a default value has been set or a runtime input option has been selected by the user, then a value is received on the channel and the current thread's node reference is reset to the node corresponding to the process following the channel communication. Otherwise, the current thread is blocked. If the process is trying to send on the channel, then the expression is evaluated, its value is written to the channel log list, and the current thread's node reference is reset to the node corresponding to the process following the channel communication.

The method creates a new thread that references the main node of the named process that is called. It also allocates space for all variables in all symbol tables of nodes in the tree representation of the named process. This thread is added to the execution list and the current thread is blocked.

The method executes a conditional process by evaluating the boolean expression in the node referenced by the current thread and resetting the reference to one of two alternative nodes based on the value of the expression.

The method evaluates the integer expression intexp in the node referenced by the current thread. The thread is removed from the execution list and its reference is reset to the node corresponding to the process following the wait term. This thread is added to the waiting list with the time stamp global time + value(intexp).

In the ALT case, the method sequentially checks each node corresponding to a process in the ALT list to determine if there is a blocked thread that wants to communicate on the channel guarding the process. As in ExecuteCommThread, ChanList.GetCommThreadID is used to check for a communicating thread.

If each channel in the ALT list is internal and no blocked thread is attempting to communicate on any channel, the current thread is not blocked, but it is moved to the end of the execution list. Unlike the case of a designated channel communication, the fact that each channel is willing to communicate is not registered in the channel table, so the thread is left unblocked to allow for possible future execution.

If a blocked thread is trying to communicate on some channel or one of the channels is an input channel, then the first channel satisfying either condition is chosen. Then either an internal or external channel communication occurs as described above in ExecuteCommThread and the references in the appropriate threads are reset to the nodes corresponding to the processes following the channel communications. In an attempt to add fairness to the scheduling algorithm, the node corresponding to the process where communication occurred is moved to the end of the node list in the ALT process.

In the OR case, the method selects a random integer k in the range 1..N, where N denotes the number of processes in the OR list. Then the reference in the current thread is reset to the node corresponding to the kth process in the list.

In the PAR case, the method creates a thread for each node corresponding to a process in the PAR list, adds these threads to the execution list, and blocks the current thread. After each new thread is run and terminates, the ThreadClass method SignalTermination is called to delete the original PAR thread.

In the SEQ case, the method creates a new thread that references the node corresponding to the first process in the SEQ list, adds this thread to the execution list, and blocks the current thread. If the new thread is run and successfully terminates, then a call to SignalTermination resets the thread reference to the node corresponding to the second process in the SEQ list. This process continues until the last process in the list is run and successfully terminates; then a call to SignalTermination deletes the original SEQ thread from the execution list.

The iterated processes ITALT, ITOR, ITPAR, and ITSEQ are executed in a manner similar to the execution of their counterparts ALT, OR, PAR, and SEQ. The expression intexp specified in the iterated process is evaluated, so by convention the specified index variable k lies in the range 0 < k < N, where N = value(intexp).

In the ITALT case, the method checks each node corresponding to a process P[k], where P denotes the process specified in the iterated construct to determine if there is a blocked thread that is trying to communicate on the channel guarding P[k]. Then the method proceeds as described in ExecuteAltThread.

In the ITOR case, the method selects a random integer 0 < k < N and resets the reference in the current thread to the node corresponding to P[k].

In the ITPAR case, a new thread is created for each 0 < k < N that references the node corresponding to P[k]. These threads are added to the execution list and the current thread is blocked. When each of these threads has run and been deleted from the execution list, the ITPAR thread is also deleted.

In the ITSEQ case, a new thread is created that references the node P[0]. This thread is added to the execution list and the current thread is blocked. When this thread has run, it will be reset to reference the node corresponding to P[1]. This process continues until the thread is runs the node corresponding to P[N - 1]. Then the thread and the ITSEQ thread are deleted from the execution list.

RunTime

This section provides additional details about the methods discussed in the preceding section as well as a summary of the primary methods that are used to execute programs.

ChanClass

For an internal channel, the method returns the threadID of any thread that is trying to communicate with the current thread; if there is no such thread, it returns currThreadID. For an external channel, the method sets an external communication flag and for an input channel the method sets the value of a variable parameter with either a default value or a runtime value entered by the user.

The method deallocates space for the values of variables associated with the thread and removes the thread from the execution list.

The method returns the threadID of the first non-blocked thread in the execution list if it exists; otherwise, it returns 0.

The method creates a thread object that references the node, allocates space for the values of variables in the node's value list, adds the thread to the execution list, and returns the threadID.

ProcessClass

The method allocates space for the values of variables in the value list of the node referenced by the thread.

The method deallocates the space for values of variables previously allocated for the thread by RunTimeAllocateSpace.

SimulationClass

The method allows an executing program to respond to user choices. It returns True if the user requests either the start or restart of execution and it returns False if the user requests the termination of execution. If the user requests a running program to idle, the method waits for further user input.

The method calls an appropriate method of the form Execute*Thread depending on the type of node referenced by the current thread.

The method increments the global time by one unit.

The method initiates the execution of the named process strProcessName.

The method performs an internal channel communication between the communicating thread and the current thread if commThreadID > 0. It performs an external communication using the current thread if commThreadID = 0.

ThreadClass

The method registers deadlock because the current thread references a node based on the STOP process. The current thread is blocked and RegisterDeadlock is called in any parent thread.

The method registers termination because the current thread references a node based on the SKIP process. If the current thread has no parent, it is deleted from the execution list. If a parent thread references a node corresponding to an uncompleted SEQ or ITSEQ construct, the current thread is reset to the node corresponding to the next process in the sequence. If the SEQ or ITSEQ construct has completed execution, then the current thread is deleted from the execution list and SignalTermination is called in the parent thread. This call is also made if the parent thread references a node corresponding to an uncompleted PAR or ITPAR construct.

WaitClass

The method adds a previously allocated thread to the waiting list maintaining an ascending sorted order based on the time stamp.

The method removes the first N threads from the waiting list.

The method adds each thread in the waiting list whose time stamp matches the current global time to the execution list. Then it calls the method DeleteFirstThreads to remove all the threads from the waiting list that satisfy this condition.

7. References Top of Page

[H] C. A. R. Hoare, Communicating Sequential Processes, Prentice-Hall, 1985.
[Also, see A.W. Roscoe, The Theory and Practice of Concurrency, Prentice Hall, 1997 and the CSP Archive.]

[O] Inmos Limited Occam 2 Reference Manual, Prentice-Hall, 1988. [Also, see the Occam Archive.]

[RS] M. D. Rice and S.B. Seidman, Using Z as a Substrate for an Architectural Style Description Language,
Technical Report CS-96-120, Department of Computer Science, Colorado State University, 1996.