1©Magee/Kramer 2nd EditionCSCI 5828: Foundationsof Software EngineeringLecture 18-19: Safety andLiveness PropertiesSlides created by Mageeand Kramer for theConcurrency textbookConcurrency: safety & liveness properties 2©Magee/Kramer 2nd EditionChapter 7Safety & LivenessPropertiesConcurrency: safety & liveness properties 3©Magee/Kramer 2nd Editionsafety & liveness propertiesConcepts: properties: true for every possible executionsafety: nothing bad happensliveness: something good eventually happens Models: safety: no reachable ERROR/STOP stateprogress: an action is eventually executedfair choice and action priorityPractice: threads and monitorsAim: property satisfaction.Concurrency: safety & liveness properties 4©Magee/Kramer 2nd Edition♦ STOP or deadlocked state (no outgoing transitions)♦ ERROR process (-1) to detect erroneous behaviour7.1 SafetyACTUATOR =(command->ACTION),ACTION =(respond->ACTUATOR|command->ERROR).Trace to ERROR:commandcommand♦ analysis using LTSA:(shortest trace)A safety property asserts that nothing bad happens.commandcommandrespond-1 0 1Concurrency: safety & liveness properties 5©Magee/Kramer 2nd EditionSafety - property specification♦ERROR conditions state what is not required (cf. exceptions).♦ in complex systems, it is usually better to specify safetyproperties by stating directly what is required.property SAFE_ACTUATOR= (command -> respond -> SAFE_ACTUATOR ).♦ analysis using LTSA as before.commandrespondcommandrespond-1 0 1Concurrency: safety & liveness properties 6©Magee/Kramer 2nd EditionSafety propertiesproperty POLITE =Property that it is polite to knock before entering a room.Traces: knockenter enterknock knock(knock->enter->POLITE).In all states, allthe actions in thealphabet of aproperty areeligible choices.knockenterknockenter-1 0 1Concurrency: safety & liveness properties 7©Magee/Kramer 2nd EditionSafety propertiesSafety property P defines a deterministicprocess that asserts that any trace includingactions in the alphabet of P, is accepted by P.Thus, if P is composed with S, then traces of actionsin the alphabet of S ∩ alphabet of P must also bevalid traces of P, otherwise ERROR is reachable.Transparency of safety properties:Since all actions in the alphabet of a property are eligiblechoices, composing a property with a set of processes does notaffect their correct behavior. However, if a behavior can occurwhich violates the safety property, then ERROR is reachable.Properties must be deterministic to be transparent.Concurrency: safety & liveness properties 8©Magee/Kramer 2nd EditionSafety properties♦ How can we specify that some action, disaster,never occurs?property CALM = STOP + {disaster}.disaster-1 0A safety property must be specified so as to includeall the acceptable, valid behaviors in its alphabet.Concurrency: safety & liveness properties 9©Magee/Kramer 2nd EditionSafety - mutual exclusionLOOP = (mutex.down -> enter -> exit -> mutex.up -> LOOP).||SEMADEMO = (p[1..3]:LOOP ||{p[1..3]}::mutex:SEMAPHORE(1)).How do wecheck that thisdoes indeedensure mutualexclusion in thecritical section?property MUTEX =(p[i:1..3].enter -> p[i].exit -> MUTEX ).||CHECK = (SEMADEMO || MUTEX).Check safety using LTSA.What happens if semaphore is initialized to 2?Concurrency: safety & liveness properties 10©Magee/Kramer 2nd Edition7.2 Single Lane Bridge problemA bridge over a river is only wide enough to permit a single lane oftraffic. Consequently, cars can only move concurrently if they aremoving in the same direction. A safety violation occurs if two carsmoving in different directions enter the bridge at the same time.Concurrency: safety & liveness properties 11©Magee/Kramer 2nd EditionSingle Lane Bridge - model♦ Events or actions of interest?enter and exit♦ Identify processes.cars and bridge♦ Identify properties.oneway♦Define each processand interactions(structure).red[ID].{enter,exit}blue[ID].{enter,exit}BRIDGEpropertyONEWAYCARSSingleLaneBridgeConcurrency: safety & liveness properties 12©Magee/Kramer 2nd EditionSingle Lane Bridge - CARS modelconst N = 3 // number of each type of carrange T = 0..N // type of car countrange ID= 1..N // car identitiesCAR = (enter->exit->CAR).To model the fact that cars cannot pass each otheron the bridge, we model a CONVOY of cars in thesame direction. We will have a red and a blue convoyof up to N cars for each direction:||CARS = (red:CONVOY || blue:CONVOY).Concurrency: safety & liveness properties 13©Magee/Kramer 2nd EditionSingle Lane Bridge - CONVOY modelNOPASS1 = C[1], //preserves entry orderC[i:ID] = ([i].enter-> C[i%N+1]).NOPASS2 = C[1], //preserves exit orderC[i:ID] = ([i].exit-> C[i%N+1]).||CONVOY = ([ID]:CAR||NOPASS1||NOPASS2).Permits1.enter 2.enter 1.exit 2.exitbut not1.enter 2.enter 2.exit 1.exitie. no overtaking.1.enter 2.enter3.enter0 1 21.exit 2.exit3.exit0 1 2Concurrency: safety & liveness properties 14©Magee/Kramer 2nd EditionSingle Lane Bridge - BRIDGE modelBRIDGE = BRIDGE[0][0], // initially emptyBRIDGE[nr:T][nb:T] = //nr is the red count, nb the blue(when(nb==0) red[ID].enter -> BRIDGE[nr+1][nb] //nb==0 | red[ID].exit -> BRIDGE[nr-1][nb] |when (nr==0) blue[ID].enter-> BRIDGE[nr][nb+1] //nr==0 | blue[ID].exit -> BRIDGE[nr][nb-1]).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 carsare only allowed to enter when the blue count is zero and vice-versa.Even when 0, exit actions permit thecar counts to be decremented. LTSAmaps these undefined states to ERROR.Concurrency: safety & liveness properties 15©Magee/Kramer 2nd EditionSingle Lane Bridge - safety property ONEWAYproperty 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 bridgeBLUE[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 bridgeWe 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 forblue cars. When the bridge is empty, either a red or a blue car may enter.Concurrency: safety & liveness
View Full Document
Unlocking...