Geekly Articles each Day
πŸ“œ ⬆️ ⬇️

Introduction to the theory of interacting sequential processes (CSP), part 2

We continue the series of articles devoted to the algebra of calculus of processes. This text is a translation and an abbreviated retelling of the initial chapters of the book by Charles E. Hoare . The theory is used to formally describe the operation of parallel systems. Examples of its practical applications are programming languages ​​such as Erlang, Go, and Limbo.

Selection


With the help of recursion and prefixes, we can describe an object with the only possible linear behavior. However, many objects are influenced by external conditions, and therefore can react to act in one way or another, depending on the situation. For example, a vending machine may have openings for one-ruble and two-ruble coins, and it will depend on the buyer which coin is inserted into the machine. Thus, if x and y are different events, then write:
(x β†’ P | y β†’ Q)

describes an object that initially participates in an event, either x or y. If an x ​​event occurs, then the object behaves further as P, if y occurs, then it will behave like Q. Because x and y are different events, the choice between P and Q is predetermined by which event the first x or y will occur. As before, we affirm the constancy of the alphabets, that is:
Ξ± (x β†’ P | y β†’ Q) = Ξ±P = Ξ±Q, implying that {x, y} βŠ† Ξ±P

Stick "|" pronounced β€œchoice”: β€œx then P select y then Q”.

Examples
  1. Possible movements of the pointer on the board:

    described as:
    (up β†’ STOP | right β†’ right β†’ up β†’ STOP)
  2. a swap machine that allows the user to choose how to swap (compare with the swap machines described earlier):
      CH5C = in5p β†’ (out1p β†’ out1p β†’ out1p β†’ out2p β†’ CH5C
         |  out2p β†’ out1p β†’ out2p β†’ CH5C)
  3. Vending machine selling either chocolate or caramel:
    VMCT = ΞΌX β€’ coin β†’ (choc β†’ X | toffee β†’ X)
  4. A more sophisticated trading machine giving customers the choice of which coins to use and what size of chocolate to get:
      VMC = (in2p β†’ (large β†’ VMC
                |  small β†’ out1p β†’ VMC)
        |  in1p β†’ (small β†’ VMC
                  |  in1p β†’ (large β†’ VMC
                            |  in1p β†’ STOP)))

    Like many complex machines, it has a constructive flaw. It is often easier to change the user instructions, rather than correct the machine itself, so let's write on the machine:
    β€œATTENTION: do not insert three one-ruble coins in a row.” (Although whom we cheat, in our conditions we will only approximate the jamming of the machine)
  5. The machine that trusts the user and allows you to try the chocolate bar and only then pay:
      VMCRED = ΞΌX β€’ (coin β†’ choc β†’ X
                |  choc β†’ coin β†’ X)
  6. To prevent losses, we will use the initial payment to obtain the privilege to use VMCRED:
    VMS2 = (coin β†’ VMCRED)

    This machine allows you to insert two coins in a row and get two chocolates in a row, but never give more chocolates than paid coins.
  7. The copying process participates in the following events:
    • in.0 - zero input
    • in.1 - unit input
    • out.0 - zero output
    • out.1 - unit output per output

    The process behavior requires repetition of input / output pairs, so we can describe it as:
      COPYBIT = ΞΌX β€’ (in.0 β†’ out.0 β†’ X
                 |  in.1 β†’ out.1 β†’ X)

    Note, the process allows you to choose what to submit to the input, while for the output there is no choice. This feature will be the main difference between the input and output of the process when discussing further the transfer of messages between processes.

The definition of choice can naturally be extended to more events, i.e .:
(x β†’ P | y β†’ Q | ... | z β†’ R)

Note that the character "|" is not an operator on a process; it will be syntactically incorrect to write P | Q, for processes P and Q. The reason for this rule is that we do not want to avoid defining the value of the following entry:
(x β†’ P | x β†’ Q)

Which seems to give a choice, but in fact does not. This problem is solved in the future by introducing uncertainty of behavior.

Thus, if x, y, z are different events, then:
(x β†’ P | y β†’ Q | z β†’ R)

should be perceived as one operator with three arguments P, Q, R. This operator is not equal to the record:
(x β†’ P | (y β†’ Q | z β†’ R))

which is syntactically incorrect.
')
To summarize, if B is a set of events and P (x) is an expression defining process for every x from B, then the expression:
(x: B β†’ P (x))

determines the process that initially proposes to choose any event y from B, after which it behaves like P (y). This expression should be pronounced " x from B then P from y ". In this construct, x is a local variable, thus:
(x: B β†’ P (x)) = (y: B β†’ P (y))

The set B defines figuratively the process menu , i.e. those actions to which the process is able to respond.

Example
  1. A process that can always participate in all events from its alphabet:
    Ξ±RUN A = A
    RUN A = (x: A β†’ RUN A )

In the special case when the menu contains only one e event:
(x: {e} β†’ P (x)) = (e β†’ P (e))

In a more special case, when the menu is empty, therefore nothing can happen:
(x: {} β†’ P (x)) = (y: {} β†’ P (y)) = STOP


Thus, the stop, the prefix and the binary choice are special cases of the general record, which will be quite convenient when formulating further the general laws concerning the processes and describing their implementation.

Indirect recursion


Regular recursion allows you to define a process as solving a single equation. This technique is easily extensible to a system of equations with more than one unknown. In order for this system to be correct it is necessary that the right-hand parts are protected and that each unknown process appears at least once in the right-hand side of any equation of the system.

Examples
  1. The drinks vending machine has two buttons, β€œorange” and β€œlemon”, clicking on which activates the setorange and setlemon events, respectively. The selection of the beverage to be poured is made by pressing the corresponding button. By pressing the dispense button, this or that drink will be poured. Before the mode was chosen, the drink will not be poured, we write this initial state as DD. Using two auxiliary processes O and L we describe the alphabet and the behavior of DD:
    Ξ±DD = Ξ±O = Ξ±L = {setorange, setlemon, dispense}
    DD = (setorange β†’ O | setlemon β†’ L)
    O = (dispense β†’ O | setlemon β†’ L | setorange β†’ O)
    L = (dispense β†’ L | setorange β†’ O | setlemon β†’ L)

    It can be seen that after selecting the mode at the very beginning (let's call it the initial setting of the machine), the machine is in one of two states, in each of which it pours a certain drink and from which it can enter the second state. You can, while in the "orange" mode, press the "orange" button, but this will not bring any effect.
  2. Using numbered variables, we can define an infinite set of equations. Let an object start on the ground and can move along the ground (let's call this action around) and can go up (let's call this action up). Being in the air, an object can either rise above (up) or descend down (down), but being on the ground it cannot sink even lower. Thus, taking the set n of natural numbers (0, 1, 2, ...) we can write the behavior of this object as:
    CT 0 = (up β†’ CT 1 | around β†’ CT 0 )
    CT n + 1 = (up β†’ CT n + 2 | down β†’ CT n )

    The first equation describes the behavior of the object on the ground, and all the others in the air.

    Thus, through indirect recursion, we have defined an infinite number of rules describing the work of our process.

Conclusion


For the convenience of reading and writing, the size of articles is somewhat reduced, I hope due to this I will be able to write them more often.

The next part will show a graphical representation of the processes, the derivation of the basic laws and the implementation of the process model. The last in the book is done with the help of lisp, but I will try to rewrite the examples on python as more familiar and understandable for many, for which it will be paid by the loss of some native transfer.

Source: https://habr.com/ru/post/139129/

More articles:


All Articles