idfk

• program execution = process
• processes consist of 1+ atomic actions
• choice = process that initially engages in either x or y, then continues as P or Q
• can also use sets of actions in place of an action at any point

  
• process is non deterministic if the same action can lead to multiple states (x -> P | x -> Q)
• indices are always finite so that the finite models/automata are finite
• use index to describe actions or states

  
• The scope of a process index variable is the process definition. The scope of an action label index is the choice element in which it occurs
• can make use of multiple index layers

  
• Alphabet of a process = the set of actions it can engage
• A process can only engage in actions in its alphabet, but not all actions will necessarily be engaged
• TERMINATED = run has run our or stop() has happened
• action a is concurrent with b if the order they are executed does not matter
• asynchronous model: concurrent executions in an arbitrary order with arbitrary relative speeds of execution
• || = concurrent execution
• by default || generates all possible interleavings (cartesian product of states)
• Shared actions must be executed at the same time by all that participate
• presence of shared actions = synchronised actions = no longer an asynchronous model
• {a1,..,ax}::P adds a a1/../ax prefix to every action label in Ps alphabet
• mutual exclusion: two processes shareing a resource, only one can use it at once
• tau actions become invisible to other processes
• interference - incorrect updates to a shared object state dur to arbitrary interleaving
• To automate search for error, combine in a TEST process that tests for and flags an erroneous trace -eg. testing a counter got updated as many times as it should have
• synchronised keyword in java makes methods mutually exclusive
• the synchronization lock in java is given to a thread for all the objects synchronised methods at once
• locking the object from the threads dealing with it is worse as relies on all users of the object to always do the same

  
• active entity = thread
• passive entity = shared object
• Monitor: encapsulated date which can only be accessed through set methods A synchronized java class with private vars
• Condition synchronisation: monitor can block thread access until a particular condition is met (eg. availableSpace > 0)
• ;active entity: initiates actions, passive entity: responds to actions
• notify - wakes a single thread; notifyAll - wakes up all threads waiting on this
• wait waits indefinitely to be awoken
• guarded actions should be implemented in java with while (!x) wait()
• semaphore: integer variable that can only be non-negative, can be decremented when x>0 and incremented up to an initialised value N
• semaphores with initialisation 1 can be used to enforce mutual exclusion by down being the claiming of the 'lock' and up being the release
• buffer - holds items from a producer process (ie. input stream) for a consumer process (ie. the program)
• bounded buffer: buffer with a fixed number of slots
• deadlock - two+ processes waiting on each other to release a lock to continue
• invariant: statement that must hold whenever a a Monitor is in a 'neutral' state (ie. not actively in use by a thread) (eg. 0 < x < N)