Esempi domande per lesame

Page 1

Question on Alloy The operating system kernel of a multiprocessor machine (with M CPUs) organizes the processes in three disjoint sets: • RUNNING: the processes that are being executed by some CPU. • READY: the processes that are ready to be executed. • WAITING: the processes that are waiting for some event from some peripheral device. Answer to the following points: A) Model in Alloy this kernel defining proper signatures and facts. Assume that processes are modeled through this signature: sig Process { } B) Model the operation Resurrect that moves a process from WAITING to READY C) Model also the following constraint: The kernel should not waste computational resources, that is, if there are READY processes, there should not be any available CPUs (that is, a CPU that is not executing any process). Solution. Note: this solution is slightly different from the one provided in the exam this exercise belongs to (and we discussed during the last lab). In the original solution there was the following fact fact { all disjoint k1, k2: Kernel | k1.ready+k1.waiting+k1.running & k2.ready+k2.waiting+k2.running = none } that, as rightly observed by one of you at the end of the lab, is constraining too much our world. If we leave it in the Alloy specification then the Resurrect predicate will be inconsistent because it will not be possible to find two kernels, k and k’, that share the same processes. sig Process { } sig CPU { busy: lone Process } sig Kernel { cpus: set CPU, ready: set Process, waiting: set Process, running: set Process } { no (ready & waiting) no (ready & running) no (waiting & running) all c: CPU | c in cpus implies (c.busy = none or c.busy in running) all p: Process | p in running implies (one c: CPU | c in cpus and p in c.busy) } 2 fact doNotWasteCPUs { all k:…