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
cs-486:homework-13 [2017/04/06 16:27]
egm [Hyman's Mutual Exclusion]
cs-486:homework-13 [2017/04/06 16:57]
egm
Line 7: Line 7:
 '''​1. (40 points)'''​ Write algorithms to compute '''​EG'''​ and '''​EU'''​ as fix-point calculations using either the [[Tools#​Cudd | Cudd]] or your library from [[Homework 12]]. Include tests that automatically check the correctness of your implementation. 20 points are allocated to the algorithms and the other 20 points are allocated to the quality of the tests. ​ '''​1. (40 points)'''​ Write algorithms to compute '''​EG'''​ and '''​EU'''​ as fix-point calculations using either the [[Tools#​Cudd | Cudd]] or your library from [[Homework 12]]. Include tests that automatically check the correctness of your implementation. 20 points are allocated to the algorithms and the other 20 points are allocated to the quality of the tests. ​
  
-'''​2. (40 points)'''​ Verify the [[Homework 13#Hyman'​s Mutual Exclusion ​| Hyman's mutual exclusion]] ​protocol below for two threads using the '''​EG'''​ and '''​EU'''​ code from the first problem. Check for mutual exclusion and fairness ​(e.g., ​a thread requesting ​the critical section ​infinitely often gets the critical section infinitely often). +'''​2. (40 points)'''​ Verify the '''​Hyman'​s Mutual Exclusion'​'' ​protocol below for two threads using the '''​EG'''​ and '''​EU'''​ code from the first problem. Check for mutual exclusion ​(e.g., there is no path where the protocol does not work) and the absence of starvation ​(e.g., ​every request for the critical section ​is eventually granted). Be sure to clearly indicate the CTL formulas for each property
  
-===Hyman'​s Mutual Exclusion===+'''​Hyman'​s Mutual Exclusion'''​
 <code c> <code c>
 void lock (int i) { void lock (int i) {
Line 25: Line 25:
 </​code>​ </​code>​
  
-'''​3. (40 points)'''​ Verify the [[Homework 13#Peterson's Mutual Exclusion | Peterson'​s mutual exclusion]] protocol below for two threads using the '''​EG'''​ and '''​EU'''​ code from the first problem. Check for mutual exclusion and fairness ​(e.g., ​a thread requesting ​the critical section ​infinitely often gets the critical section infinitely often). +'''​3. (40 points)'''​ Verify the '''​Peterson'​s mutual exclusion''' ​protocol below for two threads using the '''​EG'''​ and '''​EU'''​ code from the first problem. Check for mutual exclusion ​(e.g., there is no path where the protocol does not work) and the absence of starvation ​(e.g., ​every request for the critical section ​is eventually granted). Be sure to clearly indicate the CTL formulas for each property
  
-===Peterson'​s Mutual Exclusion===+ 
 +'''​Peterson'​s Mutual Exclusion'''​
 <code c> <code c>
 void lock (int i) { void lock (int i) {
Line 40: Line 41:
 } }
 </​code>​ </​code>​
- 
- 
  
cs-486/homework-13.txt · Last modified: 2017/04/06 16:57 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