##### Differences

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

 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] Both sides previous revision Previous revision 2017/04/06 16:57 egm 2017/04/06 16:49 egm [Problems] 2017/04/06 16:29 egm 2017/04/06 16:27 egm [Hyman's Mutual Exclusion] 2017/04/06 16:27 egm [Peterson's Mutual Exclusion] 2017/04/06 16:26 egm [Problems] 2017/04/06 16:26 egm [Hyman's Mutual Exclusion] 2017/04/06 16:26 egm [Problems] 2017/04/06 16:25 egm [Paper Pencil Problems] 2017/04/06 16:19 egm created Next revision Previous revision 2017/04/06 16:57 egm 2017/04/06 16:49 egm [Problems] 2017/04/06 16:29 egm 2017/04/06 16:27 egm [Hyman's Mutual Exclusion] 2017/04/06 16:27 egm [Peterson's Mutual Exclusion] 2017/04/06 16:26 egm [Problems] 2017/04/06 16:26 egm [Hyman's Mutual Exclusion] 2017/04/06 16:26 egm [Problems] 2017/04/06 16:25 egm [Paper Pencil Problems] 2017/04/06 16:19 egm created Last revision Both sides next revision 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 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. - ===Hyman'​s Mutual Exclusion=== + '''​Hyman'​s Mutual Exclusion'''​ void lock (int i) { void lock (int i) { Line 25: Line 25: ​ - '''​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 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. - ===Peterson'​s Mutual Exclusion=== + '''​Peterson'​s Mutual Exclusion'''​ void lock (int i) { void lock (int i) { Line 40: Line 40: } } ​ -
cs-486/homework-13.txt ยท Last modified: 2017/04/06 16:57 by egm