search
Differences
This shows you the differences between two versions of the page.
| 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. |
