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-13 [2017/04/06 16:27]
egm [Hyman's Mutual Exclusion]
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 [[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 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'''​
 <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 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'''​
 <code c> <code c>
 void lock (int i) { void lock (int i) {
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