Model-Based Approach To Designing Concurrent Systems

Model-BasedApproach toDesigning ConcurrentSystems (Part One)Kenneth M. AndersonUniversity of Colorado, BoulderCSCI 5828 — Lecture 12 — 02/18/2010 University of Colorado, 20101

Credit Where Credit isDue2Portions of these slides drawn from the course materialsdeveloped by Jeff Magee and Jeff Kramer for their excellentbookConcurrency: State Models and Java Programming, 2nd Ed.Portions are thus copyright John Wiley & Sons, Ltd. 2006

GoalsReview material from chapters 1, 2 from the optionaltextbook (Concurrency: State Models and Java Programming by Magee and Kramer)Present a model-based approach to designing concurrentsystemsWhat do we mean by model-based software engineering?Examine fundamental approach used in this book:Concepts, Modeling, PracticeFinite State Processes and Labelled Transition Systems3

More on the Authors:“The Two Jeffs”Jeff KramerDean of the Faculty of Engineering and Professor of Distributed Computingat the Department of Computing at Imperial College LondonACM Fellow; Editor of IEEE’s Transactions on Software EngineeringWinner of numerous software engineering awards including best paper andoutstanding research awardsJeff MageeProfessor at the Department of Computing at Imperial College LondonLong time member of the SE community with more than 70 journal andconference publications!This book is based on their SE research into modeling concurrency over thepast 20 years4

Ex.: Cruise Control System5RequirementsControlled by three buttonson, off, resumeTwo Threads: Engine and ControlIs the system safe?Would testing reveal all errors?How many paths through system?When ignition is switched onand on button pressed, currentspeed is recorded and systemmaintains the speed of the carat the recorded settingPressing the brake, theaccelerator, or the off buttondisables the systemPressing resume re-enables thesystem

Models to the Rescue!To answer, we need a model of the concurrent behavior ofthe system and then we need to analyze itThis is one benefit of models, they focus on one particularaspect of the world and ignore all othersConsider the model on the front of the Concurrency bookThe picture shows a real-world train next to its modelDepending on the model, you can ask certain questions andget answers that reflect the answers you would get if youasked “the real system”6

Models to the Rescue!For the train model, you might be able to askWhat color is the train? How long is it? How many cars doesit have?But notWhat’s the train’s maximum speed?How does it behave when a car derails?7

Models, continuedA model is a simplified representation of the real worldA model airplane, e.g., used in wind tunnels, models only theexternal shape of the airplaneThe reduction in scale and complexity achieved by modelingallows engineers to analyze properties of the modelThe earliest models were physical (like our model train)modern models tend to be mathematical and analyzed bycomputers8

Models, continuedEngineers use models to gain confidence in the adequacyand validity of a proposed designfocus on an aspect of interest — concurrencycan animate model to visualize a behaviorcan analyze model to verify propertiesModels support hypothesis testingwe make observations and test against our model’spredictionsif predictions match observations, we gain confidence in themodel; otherwise, we update model and try again9

Models for Concurrency10When modeling concurrencyour book makes use of a type of finite state machine knownas a labeled transition system (LTS)LTS ModelThese machines are described textually with a specificationlanguage called finite state processes (FSP)FSP Specification LanguageUsed to generate an instance of an LTS

Models for Concurrency11These machines can be displayed and analyzed by ananalysis tool called LTSANote: LTSA requires a Java 2 run time system, version 1.5.0or laterOn Windows and Mac OS systems, you can run the LTSAtool by double clicking on its jar fileNote: Its not the most intuitive piece of software, but onceyou “grok it”, it provides all of the advertised functionality

Modeling the CruiseControl System12We won’t model the entire systemlets look at a simplified exampleGiven the following specificationCRUISE (engineOn - RUNNING),RUNNING (speed - RUNNING engineOFF - CRUISE).We can generate a finite state machine that looks like this

LTSALTSA allows us to enterspecifications andgenerate state machineslike the ones on theprevious slideIt can also be used to“animate” or step throughthe state machineLets see a demoNote: animation at leftshows the problem weencountered before withthe cruise control system13

LTSA, continued14Using a modeling tool, like LTSA, allows us to understandthe concurrent behaviors of systems like the cruise controlsystem, BEFORE they are implementedThis can save a lot of time and money, as it is typically easierto test and evolve a model's behavior than it is to implementthe system in a programming language

Applying Concepts/Models via Programming15The optional textbook uses Java to enable practice of theseconceptsJava iswidely available, generally accepted, and portableprovides sound set of concurrency featuresJava is used for all examples, demo programs, andhomework exercises in the optional textbook

Summary So FarConceptsWe adopt a model-based approach for the design andconstruction of concurrent programsModelsfinite state machines to represent concurrent behaviorPracticeBook uses Java for constructing concurrent programsWe will be presenting numerous examples to illustrateconcepts, models and demonstration programs16

Modeling SequentialProcesses17We structure complex systems as sets of simpler activitieseach represented as a sequential processProcesses can overlap or be concurrent, so asto reflect the concurrency inherent in the physical worldor to offload time-consuming tasksor to manage communications and/or other devicesDesigning concurrent software can be complex/error proneA rigorous engineering approach is essential

Overall ApproachConcept of a process asa sequence of actionsModel processes asfinite state machinesProgram processes asthreads in Java18

Modeling ProcessesModels are described using state machinesLabeled Transition System (LTS)Described textually as finite state processes (FSP)They are displayed and analyzed by the LTSA toolSummaryFSP: textual formLTS: data structureLTSA: visualizer and analyzer19

Modeling Processes20A process is the execution of a sequential program. It ismodeled as a finite state machine that moves from state tostate by executing a sequence of atomic actionsTo the right is a “light switch”it has two states and two actionswhat does state zero represent?A trace is a sequence of actionsFor the light switch: on off on off on

Specifying a process21FSP — action prefixIf x is an action and P a process then ( x P ) describes aprocess that initially engages in the action x and then behavesexactly as described by P. i.e. ( x P ) is also a process.ONESHOT (once - STOP).STOP is a predefined processthat tells LTSA to halt.ONESHOT is a process; it executes “once” before haltingConvention: actions begin with lowercase letters; PROCESSES useall uppercase letters

Repetitive behavior22Repetitive behavior uses recursion:SWITCH OFF,OFF (on - ON),ON (off - OFF).You can apply substitutionSWITCH OFF,OFF (on - (off - OFF)).And again, to get a succinct definitionSWITCH (on - off - SWITCH).All threeproduce theabove LTS

Animation3. viewyourtracehere231. clickactions2. see updates;(LTSA is notperfect; it can’talways showthe updates)

Simple ExampleTRAFFICLIGHT (red - green - yellow - TRAFFICLIGHT).Tracered green yellow red green yellow 24

Adding Choice25If x and y are actions then( x P y Q) is a processwhich initially engages ineither of the actions x or y.DRINKS (red - coffee- DRINKS blue - tea - DRINKS).red and blue are consideredinput actions; coffee and teaare output actionsAn input action is one whichparticipates in a choice; someonehas to select an action before theprocess can go on.

Nondeterministic ChoiceProcess (x P x Q) describes a process which engages in xand then behaves as either P or Q.As you can see, we have the same action on multiple branchesCOIN (toss - HEADS toss - TAILS),HEADS (heads - COIN),TAILS (tails - COIN).Tossing a coin.In this case, LTSAwill randomly select a branchto execute.26

Modeling Failure27We can use nondeterminism to model failureHere we want to model a communication channel that issometimes unreliable; an input can sometimes fail to producean outputCHAN (in - CHAN in - out - CHAN).

Adding modeling power28In order to increase the power of our models, we can addindexes to both actions and processesWe can add an index to an action, like this in[i : 0 . 3] which requires us to pick a value for the index when weexecute the actionThe index can then be referenced in later actions, carryingthe value we pickedout[i]

ExampleBUFF (in[i: 0.3] - out[i] - BUFF).Single slot bufferwhat goes inmust come out29

indexes are shortcutsNote, this:BUFF (in[i: 0.3] - out[i] - BUFF).is equivalent to this:BUFF (in[0]- out[0]- BUFF in[1]- out[1]- BUFF in[2]- out[2]- BUFF in[3]- out[3]- BUFF).indexed actions simply expand to all possible choicesbehind the scenes30

Magic Numbers31In this processBUFF (in[i: 0.3] - out[i] - BUFF).“3” is a magic numberWe can add flexibility to our models via indexed processesBUFF(N 3) (in[i:0.N]- out[i]- BUFF).Now we can change N to whatever value we need

Computation32Indexes can be used to model calculationconst N 1range T 0.Nrange R 0.2*NSUM (in[a:T][b:T]- TOTAL[a b]),TOTAL[s:R] (out[s]- SUM).Here, our choices for indexes a and b influence the startingvalue s for process TOTAL; a b is calculated and passedto TOTAL, setting the value for index s

LTS for SUM33

Guarded Actions34The choice (when B x - P y - Q) means that when theguard B is true, then the actions x and y are both eligible tobe chosen, otherwise only y can be selected.COUNT(N 3) COUNT[0],COUNT[i:0.N] ( when(i N) inc- COUNT[i 1] when(i 0) dec- COUNT[i-1]).

Process Alphabets35The alphabet of a process is the set of actions in which itcan engage; LTSA can show a process alphabet on requestProcess alphabets are implicitly defined by the actions inthe process definition.COUNTDOWN (N 3) (start- COUNTDOWN[N]),COUNTDOWN[i:0.N] ( when(i 0) tick- COUNTDOWN[i-1] when(i 0)beep- STOP stop- STOP).The alphabet of COUNTDOWN is “start”, “tick”, “beep”,and “stop”

Implementing ModelsImplementing a model is typically straightforwardpublic void start() {counter new Thread(this);i N; counter.start();}public void stop() {counter null;}public void run() {while(true) {if (counter null) return;if (i 0) { tick(); --i; }if (i 0) { beep(); return;}}}Implementation ofCOUNTDOWNimagine this placed insideof a class that implementsRunnable36

threads in JavaA Thread class manages a single sequential thread of control.Threads may be created and deleted dynamically.Threadrun()37The Thread class executes instructions from its methodrun(). The actual code executed depends on theimplementation provided for run() in a derived class.MyThreadrun()class MyThread extends Thread {public void run() {//.}}Creating a thread object:Thread a new MyThread();Concurrency: processes & threads26 Magee/Kramer 2nd Edition

threads in JavaSince Java does not permit multiple inheritance, we oftenimplement the run() method in a class not derived from Thread butfrom the interface Runnable.targetRunnablerun()MyRunrun()Concurrency: processes & threadsThreadpublic interface Runnable {public abstract void run();}class MyRun implements Runnable{public void run() {//.}}Creating a thread object:27Thread b new Thread(newMyRun()); Magee/Kramer2 Editionnd38