Differences

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

Link to this comparison view

Both sides previous revision Previous revision
Last revision Both sides next revision
cs-486:homework-13 [2017/04/06 16:29]
egm
cs-486:homework-13 [2017/04/06 16:49]
egm [Problems]
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 '''​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 existence of ''​fair''​ path (e.g., some path exists where both threads access ​the critical section infinitely often). Be sure to clearly indicate the CTL formulas for each property
  
 '''​Hyman'​s Mutual Exclusion'''​ '''​Hyman'​s Mutual Exclusion'''​
Line 25: Line 25:
 </​code>​ </​code>​
  
-'''​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 ​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 existence of ''​fair''​ path (e.g., some path exists where both threads access ​the critical section infinitely often). Be sure to clearly indicate the CTL formulas for each property
  
 '''​Peterson'​s Mutual Exclusion'''​ '''​Peterson'​s Mutual Exclusion'''​
Line 40: Line 40:
 } }
 </​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