Environment Modeling in Quasi-Static SchedulingOutlineMotivationQSS InputQSS AlgorithmExampleEnvironment ModelProblemsEnvironment ModelingApproachesAssume, then GuaranteeGuarantee FirstExample (I)Example (II)ExpressivenessFuture WorkEnvironment Modeling in Quasi-Static SchedulingEE249 ProjectDonald ChaiMentors: Alex Kondratyev, Yoshi WatanabeEnvironment Modeling in QSS 2OutlineMotivationMethod for QSSProblemsEnvironment ModelingConclusionsEnvironment Modeling in QSS 3MotivationSchedule some set of processes on one CPUDynamic scheduling requires overhead for communication and context switchingStatic scheduling minimizes context switching overhead—scheduling for BDF is undecidableQSS is a compromise, somewhat like cooperative multitasking by inserting sleepsEnvironment Modeling in QSS 4QSS InputSpecification comes in FlowC (YAPI framework)Sequential processes communicate over FIFO channels, a process may READ, WRITESELECT nondeterministically from a set of ready input portsEnvironment Modeling in QSS 5QSS AlgorithmFlowC descriptions are translated into a Petri NetThe Petri Net is partitioned into single source schedules.QSS is a game between the scheduler and the environment.Environment Modeling in QSS 6ExampleA system that is not schedulableIs schedulable in the right environmentFrom Clarisó, Cortadella, Kondratyev, Lavagno, Passerone, Watanabe, INT2002Environment Modeling in QSS 7Environment ModelInput ports may be fully uncontrollable or fully controllableNo known relation between inputsOutput ports are always fully controllableEnvironment Modeling in QSS 8ProblemsBoundedness (previous example)Deadlock (two processes B,A, sequenced by the environment into A,B)Interference (arbitration)Environment Modeling in QSS 9Environment ModelingThe form we should use is asymmetric:Sysabs is QSS schedulable · is the trace containment relationAssume-guarantee proof rule states:Environment Modeling in QSS 10ApproachesAssume some environment during scheduling, check this.Construct an abstract environment. (correct by construction)Restrict the power of our model of computation.Environment Modeling in QSS 11Assume, then Guarantee“Try and see”Basically we generate a trace of the assumptions madeNot very robust, and very compute intensive42Environment Modeling in QSS 12Guarantee FirstThe environment is abstracted using a set of reduction rulesCan be done via trace algebra projection, but may be overkillEnvironment Modeling in QSS 13Example (I)Arbiter Module Arbiter + ProcessEnvironment Modeling in QSS 14Example (II)SELECT is reduced More reductionsEnvironment Modeling in QSS 15ExpressivenessProcesses look like FCPNs (free choice from if statements)When add READs and SELECTs, looks more like asymmetric choiceEnvironment Modeling in QSS 16Future WorkPartitioning is used extensively for equivalence checking of circuits. What would be good places to partition the
View Full Document
Unlocking...