Concurrency safety liveness properties 1 Magee Kramer 2nd Edition Concurrency safety liveness properties 2 Magee Kramer 2nd Edition Chapter 7 Safety Liveness Properties Concurrency safety liveness properties 3 Magee Kramer 2nd Edition safety liveness properties Concepts properties true for every possible execution safety nothing bad happens liveness something good eventually happens Models safety no reachable ERROR STOP state progress an action is eventually executed fair choice and action priority Practice threads and monitors Aim property satisfaction Concurrency safety liveness properties 4 Magee Kramer 2nd Edition 7 1 Safety A safety property asserts that nothing bad happens STOP or deadlocked state no outgoing transitions ERROR process 1 to detect erroneous behaviour command 1 0 1 respond command analysis using LTSA shortest trace Concurrency safety liveness properties ACTUATOR command ACTION ACTION respond ACTUATOR command ERROR Trace to ERROR command command 5 Magee Kramer 2nd Edition Safety property specification ERROR conditions state what is not required as done on prior slide In complex systems it is usually better to specify safety properties by stating directly what is required command 1 0 respond 1 respond property SAFE ACTUATOR command respond SAFE ACTUATOR command analysis using LTSA as before Concurrency safety liveness properties 6 Magee Kramer 2nd Edition Safety properties Property that it is polite to knock before entering a room Traces knock enter enter knock knock property POLITE knock enter POLITE In all states all the actions in the alphabet of a property are eligible choices Concurrency safety liveness properties 1 knock 0 enter 1 enter knock 7 Magee Kramer 2nd Edition Safety properties Safety property P defines a deterministic process that asserts that any trace including actions in the alphabet of P is accepted by P Thus if P is composed with S then traces of actions in the alphabet of S alphabet of P must also be valid traces of P otherwise ERROR is reachable Transparency of safety properties Since all actions in the alphabet of a property are eligible choices composing a property with a set of processes does not affect their correct behavior However if a behavior can occur which violates the safety property then ERROR is reachable Properties must be deterministic to be transparent Concurrency safety liveness properties 8 Magee Kramer 2nd Edition Safety properties How can we specify that some action disaster never occurs 1 0 disaster property CALM STOP disaster A safety property must be specified so as to include all the acceptable valid behaviors in its alphabet Concurrency safety liveness properties 9 Magee Kramer 2nd Edition Simple Example HIDEIT a CD CD c EF d GH EF b e HIDEIT f IJ GH g b HIDEIT h a HIDEIT IJ i b HIDEIT j b HIDEIT Imagine that we cared that in the process HIDEIT the action a always comes before the action b How would we check if this is true Write a safety property and have LTSA check it property AB a b AB Concurrency safety liveness properties 10 Magee Kramer 2nd Edition Safety mutual exclusion more complex example LOOP mutex down enter exit mutex up LOOP SEMADEMO p 1 3 LOOP p 1 3 mutex SEMAPHORE 1 How do we check property MUTEX p i 1 3 enter that this does p i exit indeed ensure MUTEX mutual exclusion CHECK SEMADEMO MUTEX in the critical section Check safety using LTSA What happens if semaphore is initialized to 2 Concurrency safety liveness properties 11 Magee Kramer 2nd Edition 7 2 Single Lane Bridge problem A bridge over a river is only wide enough to permit a single lane of traffic Consequently cars can only move concurrently if they are moving in the same direction A safety violation occurs if two cars moving in different directions enter the bridge at the same time Concurrency safety liveness properties 12 Magee Kramer 2nd Edition Single Lane Bridge model Events or actions of interest enter and exit Identify processes property CARS cars and bridge ONEWAY Identify properties oneway Define each process blue ID Single red ID enter exit enter exit Lane and interactions BRIDGE Bridge structure Concurrency safety liveness properties 13 Magee Kramer 2nd Edition Single Lane Bridge CARS model const N 3 range T 0 N range ID 1 N number of each type of car type of car count car identities CAR enter exit CAR To model the fact that cars cannot pass each other on the bridge we model a CONVOY of cars in the same direction We will have a red and a blue convoy of up to N cars for each direction CARS red CONVOY blue CONVOY Concurrency safety liveness properties 14 Magee Kramer 2nd Edition Single Lane Bridge CONVOY model NOPASS1 C i ID NOPASS2 C i ID C 1 preserves entry order i enter C i N 1 C 1 preserves exit order i exit C i N 1 CONVOY ID CAR NOPASS1 NOPASS2 1 enter 0 2 enter 1 3 enter Permits but not 1 exit 2 0 2 exit 1 2 3 exit 1 enter 2 enter 1 exit 2 exit 1 enter 2 enter 2 exit 1 exit ie no overtaking Concurrency safety liveness properties 15 Magee Kramer 2nd Edition Single Lane Bridge BRIDGE model Cars can move concurrently on the bridge only if in the same direction The bridge maintains counts of blue and red cars on the bridge Red cars are only allowed to enter when the blue count is zero and vice versa BRIDGE BRIDGE 0 0 BRIDGE nr T nb T when nb 0 red ID enter red ID exit when nr 0 blue ID enter blue ID exit Concurrency safety liveness properties initially empty nr is the red count nb the blue BRIDGE nr 1 nb BRIDGE nr 1 nb nb 0 BRIDGE nr nb 1 BRIDGE nr nb 1 nr 0 Even when 0 exit actions permit the car counts to be decremented LTSA maps these undefined states to ERROR 16 Magee Kramer 2nd Edition Single Lane Bridge safety property ONEWAY We now specify a safety property to check that cars do not collide While red cars are on the bridge only red cars can enter similarly for blue cars When the bridge is empty either a red or a blue car may enter property ONEWAY red ID enter RED 1 blue ID enter BLUE 1 RED i ID red ID enter RED i 1 when i 1 red ID exit ONEWAY when i 1 red ID exit RED i 1 i is a count of red cars on the bridge BLUE i ID blue ID enter BLUE i 1 when i 1 blue ID exit ONEWAY when i 1 blue ID exit BLUE i 1 i is a count of blue cars on the bridge Concurrency safety liveness properties 17 Magee Kramer 2nd Edition Single Lane Bridge model analysis SingleLaneBridge CARS BRIDGE ONEWAY Is the safety property ONEWAY violated No deadlocks errors SingleLaneBridge CARS ONEWAY Without the BRIDGE contraints is the Trace to property
View Full Document
Unlocking...