Differences

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

Link to this comparison view

Both sides previous revision Previous revision
cs-486:homework-13 [2017/04/06 22:49]
egm [Problems]
cs-486:homework-13 [2017/04/06 22:57] (current)
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 '''​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 a ''​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. ​+'''​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'''​
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 (e.g., there is no path where the protocol does not work) and the existence ​of a ''​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. ​+'''​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'''​
Line 40: Line 41:
 } }
 </​code>​ </​code>​
- 
  
cs-486/homework-13.txt · Last modified: 2017/04/06 22: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