mpc

({NewPort <s> <p>}, E)

does the following:

1. Create a fresh port name n.
2. Bind E(<p>) and n in the single assignment store.
3. If the binding is successful, then (1) Add the pair E(<s>) : E(<s>) to the mutable store M.
4. Else (1) Raise an error condition.

({Send <p> <y>), E)

1. If E(<p>) is determined (1) Uf E(<p>) is not bound to a port, then raise error (2) If the mutable store contains E(<p>):z
   1. Create a new variable z' in the store
   2. Update the mutable store to be E(<p>):z'
   3. Create a new list pair E(<y>)|z' and bind z with it in the single assignment store.
2. Else, suspend execution.

In a correct port, the end of the stream should be read-only. We have not implemented this. This can be implemented with "Secure ADT"s.

1. Extend the definition of reachability. If x:y is in the mutable store, and x is reachable, then y is reachable as well.
2. If the port variable x becomes unreachable, and the mutable store contains x:y, then y becomes unreachable as well.

If there is no internal state, then the new port is simple.

fun {NewPortObject2 P}
Sin in
  thread
    for Msg in Sin do
      {P Msg}
    end
  end
  {NewPort Sin}
end

However, we can also consider ports which have an internal state, similar to that in the case of stream objects.

fun {NewPortObject InitState F}
Sin Sout in
  thread {FoldL Sin F InitState Sout}
  {NewPort Sin}
end

Using this, we can program simple message passing protocol.

---

e.g. from the text

3 players tossing a ball to each other. Each recepient tosses the ball to one of the other two, chosen at random.

Each player is a stateless port object.

Code: Players.oz

---

Proving a program correct consists of two parts.

1. Show that the port object is correct. Each port object defines a data abstraction. The abstraction should have an invariant assertion. Since the inside of a port is declarative, we can use the techniques for declarative programs.

   Each port object has a single thread. Hence it's operations are executed sequentially. Hence mathematical induction provides a way to assert invariants.

   • When the port object is first created, the invariant is satisfied.
   • If the assertion is satisfied before a message is handled, then the assertion is satisfied after it is handled.
2. Show that the program using the port objects is correct. This involves interacting ports. We have to determine the possible sequences of messages that each port can receive. First, we classify the events - message sends, message receives, internal state changes.

   Then we can consider the program as a state transition system. Reasoning about the correctness of such transition systems is complicated.

---

|\ |       Method is port's message-handling procedure.
| \|       A client sends a request to a server and waits for a reply.
|  |
|  |       ---------Server---------
| /|       proc {ServerProcedure Msg}
|/ |         case Msg
|  |           of append(X Y Z) then {Append X Y Z}
|\ |         end
| \|       end
|  |       Server = {NewPort2 ServerProcedure}
| /|       ------------------------
|/ |
|  |       ---------Client---------
C  S       proc {ClientProcedure Msg}
             case Msg
               of work(X Y Z R) then
                 local W in
                   {Send Server append(X Y W)}
                   {Wait W}
                   {Send Server append(W Z R)}
                 end
               end
             end
           end
           Client = {NewPort2 ClientProcedure}
           declare R
           {Browse {Send Client work([1 2] [3] [4] R)}
           -------------------------

The client refers directly to the server, but not vice versa.

This is a synchronous call.

|     |
|\    |       The client proceeds immediately after sending the request, 
| \   |       without waiting  for the server response.
|  \  |
|\  \ |
| \  \|
|  \  |
|   \/|
|   /\|
|  /  |
| /  /|
|/  / |
|  /  |
| /   |
|/    |
|     |
C     S

---

TBD

TBD

proc {ConcFilter L F ?L2}
   Send
in
   {NewPort L2 Send}
   {Barrier
       {Map L
            fun {$ X}
               proc {$}
                   if {F X} then {Send X} end
               end
            end}}
end

---

In this section, we will try to describe the semantics of the Erlang receive operation, in terms of equivalent Oz statements.

---