From 40dbd4e5cc0a28711af6f9de4c27ce236072d3dc Mon Sep 17 00:00:00 2001 From: Camil Staps Date: Wed, 9 Sep 2015 22:17:18 +0200 Subject: Organisation; assignment 2 --- assignment2/assignment2.txt | 8 ++++ assignment2/hyman.q | 6 +++ assignment2/hyman.xml | 10 +++++ assignment2/hyman.xtr | 95 +++++++++++++++++++++++++++++++++++++++++++++ 4 files changed, 119 insertions(+) create mode 100644 assignment2/assignment2.txt create mode 100644 assignment2/hyman.q create mode 100644 assignment2/hyman.xml create mode 100644 assignment2/hyman.xtr (limited to 'assignment2') diff --git a/assignment2/assignment2.txt b/assignment2/assignment2.txt new file mode 100644 index 0000000..ceee4fa --- /dev/null +++ b/assignment2/assignment2.txt @@ -0,0 +1,8 @@ +Camil Staps (s4498062) + +1. +De `not blocked[1-i]' en `turn := 1' zijn twee stappen. Als daartussen een context switch plaatsvindt, kunnen beide processen tegelijkertijd in de kritieke sectie terechtkomen. Maken we hetzelfde model waarbij we deze twee stappen samenvoegen, dan is er geen probleem. Zie hyman.xml, hyman.q, hyman.trx. + +2. +Stel dat proces 1 zich in de kritieke sectie bevindt. Als er nu om wat voor reden dan ook nooit een context switch plaatsvindt op het moment dat proces 1 zich in staat `Start' bevindt, dan zal proces 2 nooit opmerken dat proces 1 zijn blocked bit op 0 zet. Proces 2 zou in dat geval dus nooit in de kritieke sectie terechtkomen, maar continue in `WaitBlocked' blijven hangen. + diff --git a/assignment2/hyman.q b/assignment2/hyman.q new file mode 100644 index 0000000..0bd1a71 --- /dev/null +++ b/assignment2/hyman.q @@ -0,0 +1,6 @@ +//This file was generated from (Commercial) UPPAAL 4.0.14 (rev. 5615), May 2014 + +/* + +*/ +E<> (p1.CriticalSection && p2.CriticalSection) diff --git a/assignment2/hyman.xml b/assignment2/hyman.xml new file mode 100644 index 0000000..fb22f25 --- /dev/null +++ b/assignment2/hyman.xml @@ -0,0 +1,10 @@ +// Place global declarations here. +typedef int[0,1] ids; +bool blocked[ids]; +int turn = 0;// Place template instantiations here. +p1 = Process(0); +p2 = Process(1); + +// List one or more processes to be composed into a system. +system p1, p2; \ No newline at end of file diff --git a/assignment2/hyman.xtr b/assignment2/hyman.xtr new file mode 100644 index 0000000..5dfbf2a --- /dev/null +++ b/assignment2/hyman.xtr @@ -0,0 +1,95 @@ +4 +4 +. +. +0 +0 +0 +0 +1 +. +4 +3 +. +. +0 +1 +0 +0 +1 +. +1 7 +. +4 +1 +. +. +0 +1 +0 +0 +1 +. +1 4 +. +4 +0 +. +. +0 +1 +0 +0 +1 +. +1 2 +. +3 +0 +. +. +1 +1 +0 +0 +1 +. +0 7 +. +2 +0 +. +. +1 +1 +0 +0 +1 +. +0 6 +. +2 +3 +. +. +1 +1 +1 +0 +1 +. +1 1 +. +2 +2 +. +. +1 +1 +1 +0 +1 +. +1 6 +. +. -- cgit v1.2.3