[cs63201] Execution Sematics

[Mikhail Nesterenko]

>
> The slides never actually mention execution semantics by the names
> we talked about in class earlier today. I think they're referred to
> as Fully Synchronous, Partially Synchronous, and Fully
> Asynchronous. Fully Synchronous sounds like interleaving semantics
> to me, Asynchronous is Power Set? What would Partially Synchronous
> be?

Sorry to be late with this. Synchrony assumptions are as follows.

- synchronous - all enabled guarded commands are executed
  simultaneously. That is:

  		.... state I ---> state I+1 .....

  All guarded commands that are enabled in state I are executed to
  produce state I+1

- partial synchronous - there is a limit on how long (in the number
  of states) the guarded command can be enabled before it is executed.
  For example: every guarded command either gets disabled or executed
  in 5 states.

  Actually, there are variants of these model where this limit is
  known or unknown to the program. If the program knows the limit,
  it can exploit it to determine whether the message was sent.

- fully asynchronous - no limit. This is the synchrony assumption we
  usually use.

Now, execution semantics, powerset and interleaving, can be used in
conjunction with the synchrony assumption. We can use powerset or
interleaving either for partially or fully synchronous systems. The
only exception is synchronous systems: the only execution semantics
there is powerset.

Thanks,
--
Mikhail