Differences

This shows you the differences between two versions of the page.

Link to this comparison view

Both sides previous revision Previous revision
Next revision
Previous revision
Last revision Both sides next revision
cs-486:homework-2 [2017/01/26 09:36]
egm
cs-486:homework-2 [2017/10/09 16:05]
egm [Problems]
Line 9: Line 9:
 '''​2. (30 points)'''​ Answer problems 2(a) through 2(b) from the [http://​spinroot.com/​spin/​Man/​1_Exercises.html SPIN Verification Examples and Exercises]. Note that the PROMELA code does not include all the transitions in the figure and it is missing transitions as well. Part of your answer should modify the PROMELA to match the diagrams. Also, for the second part, b, modify the PROMELA in S1 for  both terminal A and terminal B. '''​2. (30 points)'''​ Answer problems 2(a) through 2(b) from the [http://​spinroot.com/​spin/​Man/​1_Exercises.html SPIN Verification Examples and Exercises]. Note that the PROMELA code does not include all the transitions in the figure and it is missing transitions as well. Part of your answer should modify the PROMELA to match the diagrams. Also, for the second part, b, modify the PROMELA in S1 for  both terminal A and terminal B.
  
-'''​3. (50 points)'''​ This problem comes from [https://​d1b10bmlvqabco.cloudfront.net/​attach/​i4libjkuz9io1/​i4licnd7ihy2nh/​i5zqbdqd68yu/​Assignment_4_CS118_2015.pdf CalTech'​s CS 118 Assignment 4]. Consider a distributed system that consists of five producers, one scheduler, and two consumers. Each producer has two tasks that need to be completed by a consumer. For each task, a producer sends a request to the scheduler. The scheduler has a queue to store up to five incoming producer requests. The scheduler, upon receiving a request, assigns the task to one of the consumers. The two consumers have their own separate queue of outstanding tasks. A consumer can only service one request at a time, but it can have up to two outstanding tasks waiting in the queue. Consumers do not acknowledge completion of tasks.+'''​3. (20 points)'''​ This problem comes from [https://​d1b10bmlvqabco.cloudfront.net/​attach/​i4libjkuz9io1/​i4licnd7ihy2nh/​i5zqbdqd68yu/​Assignment_4_CS118_2015.pdf CalTech'​s CS 118 Assignment 4]. Consider a distributed system that consists of five producers, one scheduler, and two consumers. Each producer has two tasks that need to be completed by a consumer. For each task, a producer sends a request to the scheduler. The scheduler has a queue to store up to five incoming producer requests. The scheduler, upon receiving a request, assigns the task to one of the consumers. The two consumers have their own separate queue of outstanding tasks. A consumer can only service one request at a time, but it can have up to two outstanding tasks waiting in the queue. Consumers do not acknowledge completion of tasks.
  
 The definitions for prototypes ''​Producer'',​ ''​Consumer'',​ and ''​init''​ are provided below. Write the definition for prototype ''​Scheduler''​ for assigning tasks to the consumers. The scheduler is constrained by the following property when assigning tasks: it must balance the workloads of the two consumers. That is, a new task is always assigned to the consumer who has the fewest number of outstanding tasks in its queue. If the number of tasks currently assigned is equal, then the task could be assigned to either consumer. Prove with SPIN that your solution has the right properties. The definitions for prototypes ''​Producer'',​ ''​Consumer'',​ and ''​init''​ are provided below. Write the definition for prototype ''​Scheduler''​ for assigning tasks to the consumers. The scheduler is constrained by the following property when assigning tasks: it must balance the workloads of the two consumers. That is, a new task is always assigned to the consumer who has the fewest number of outstanding tasks in its queue. If the number of tasks currently assigned is equal, then the task could be assigned to either consumer. Prove with SPIN that your solution has the right properties.
Line 26: Line 26:
   do   do
   :: schedToCons[me]?​task(you)   :: schedToCons[me]?​task(you)
 +  :: timeout -> break
   od   od
 } }
Line 45: Line 46:
 </​code>​ </​code>​
  
-'''​4. (30 points)'''​ Write a PROMELA verification model for [https://​www.risc.jku.at/​software/​daj/​TermDetect/​ Dikstra'​s Token Termination Algorithm] (another [http://​people.cs.aau.dk/​~adavid/​teaching/​MVP-10/​17-Termination-lect14.pdf presentation]) and use SPIN to prove that the verification model is correct. Make the verification model be parameterized by '''​N'''​ the number of nodes participating in the system.+'''​4. (50 points)'''​ Write a PROMELA verification model for [https://​www.risc.jku.at/​software/​daj/​TermDetect/​ Dikstra'​s Token Termination Algorithm] (another [http://​people.cs.aau.dk/​~adavid/​teaching/​MVP-10/​17-Termination-lect14.pdf presentation]) and use SPIN to prove that the verification model is correct. Make the verification model be parameterized by '''​N'''​ the number of nodes participating in the system.
cs-486/homework-2.txt ยท Last modified: 2018/09/04 12:38 by egm
Back to top
CC Attribution-Share Alike 4.0 International
chimeric.de = chi`s home Valid CSS Driven by DokuWiki do yourself a favour and use a real browser - get firefox!! Recent changes RSS feed Valid XHTML 1.0