Re: A CSP model for Java threads

[P.H.Welch@xxxxxxxxx]

Jeremy, as usual, put his finger on a crucial point to which my answer
was a little incomplete:

> > * The standard semantics of CSP don't allow for any state, so you
> > shouldn't really introduce variables to represent synchronisation count.
> > Perhaps you could use processes to represent the count variables.
> 
> I know ... I did mention that, perhaps, those counts should be modelled
> as processes.  But they belong to the user threads, so I would envisage
> the process model of a user thread just to carry this count around as
> an extra subscript (or index), which is one way CSP can capture the notion
> of state.

In the case of those "count[o][me]" variables, carrying them around as extra
subscripts/parameters/indices of the process modelling the user thread works
because they represent *unshared* internal state of that process.

However, that's not the case for the state represented by variables in users'
monitor Objects.  That state is *shared* between all user threads that access
the (passive) monitor.

The CSP model for Java threads (so far) formalises just the synchronisation
rules relied on by Java applications to protect that shared data.  We haven't
modelled the actual access and update of that state by the user threads.
If we don't model that shared state information, the key subtleties of
the monitor algorithms will be missed and analysis will show all sorts
of phantom race hazards and deadlocks!

We can't model that state by process subscripts/parameters/indices, since
it is shared by more than one process.  The simplest idea is to model each
(monitor) variable, representing that shared state, by a process.  This is
easy to do using CSP channel events:


  Let "Variables" be an ennumeration of all (monitor) shared variables.

  We have the following sets of channels:

    read  = { read[v][t] | v in Variables, t in Threads}
    write = (write[v][t] | v in Variables, t in Threads}
  
  We have the following processes:

    VARIABLE = {VARIABLE[v] | v in Variables}
  
  where:

    alpha (VARIABLE[v]) = { read[v][t] | t in Threads} union
			  (write[v][t] | t in Threads}
    
    VARIABLE[v] = VARIABLE[v][initial-v]
  
  where "initial-v" is some (user-defined) initial value for "v" and:

    alpha (VARIABLE[v][value] = alpha (VARIABLE[v])

    VARIABLE[v][value] =
    
      ([] (read[v][t] ! value --> VARIABLE[v][value] | t in Threads)

      []

      ([] (write[v][t] ? x --> VARIABLE[v][x] | t in Threads)


Of course, for modelling any particular shared (monitor) variable, the set
"Threads" in the above could be restricted to just those threads that might
access/update it.  [And occamists could introduce "request[v][t]" channels
so that "VARIABLE[v][value]" doesn't have to choose over output guards :-).]

For example, if we had a shared integer variable "VARIABLE{n]", then its
incrementing by any thread, "me", that can see it is modelled by:

  read[v][me] ? x --> write[v][me] ! (x + 1) --> SKIP  // LOAD v; INC; STORE v

As for Java shared variables, this incrementing is not atomic and may be
interleaved with other accesses/updates by other threads.  In which case,
the Java program had better protect all such access/update within some
`synchronized' block (and, if necessary, some `wait's and `notify's) on
a common Object.  The previously posted model captures all of that and
we should now be able to build CSP models that *do* reflect the shared state
inside Java monitors and start proving things.

For the JCSP channel monitors, this shared state is represented by just
three variables:

  channel_hold  (Object or int -- initially anything))
  channel_empty (Boolean -- initially true)
  alt           (Alternative -- initially null)

For the JCSP Alternative monitor, there is just one shared variable:

  state         (int -- initially `inactive')

The possible values for "state" are `inactive', `enabling', `ready' and
`waiting'.

Now, with the aid of just a few beers, we should start to be able to prove
something!


Peter.