##### 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:57]egm 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 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'''​ 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 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'''​ void lock (int i) { void lock (int i) { Line 40: Line 41: } } ​ - -