CSSE7610 Assignment 1: Mutual exclusion
1. Prove the correctness of Peterson’s algorithm using deductive techniques. Given the following
invariants similar to those of Dekker’s algorithm
(a) (last = 1) ∨ (last = 2)
(b) p3..6 ⇔ wantp
(c) q3..6 ⇔ wantq
first show that
(p4 ∧ q5) ⇒ (wantq ∧ last = 1),
(p5 ∧ q4) ⇒ (wantp ∧ last = 2)
are also invariants, and then use them to prove mutual exclusion holds. Then state the
condition for freedom from starvation for process p and provide a proof that it holds.
Deliverable: A file peterson.pdf containing the correctness arguments, and your name and
2. (a) Write a Promela specification for a modified version of Peterson’s algorithm that does
not have more than one critical reference in any atomic statement.
(b) Use Spin to prove that the algorithm is still correct: use an assertion to prove mutual
exclusion, and an LTL property to prove freedom from starvation.
Deliverables: A file peterson.pml containing the Promela specification and including comments detailing how you carried out the proofs and stating any LTL properties required.
The pml file must include your name and student number (as a comment).
3. Speed is a card game where the players simultaneously try to get rid of all their cards.
In this version of the game, we have 2 players and use a pack of 60 cards. Each card has
between 1 and 5 motifs of a particular shape and colour on it. For example, a card may
have 4 green diamonds, or it may have 5 blue circles, or it may have 1 red square. We will
assume there are 6 different shapes and 6 different colours, and that the pack has a random
selection of 60 such cards which may contain duplicate cards.
Each player is dealt a pile of 29 cards and the remaining two cards are placed face up in front
of the players. The players pick up the top 3 cards from their pile and must simultaneously
try to place them on one of the cards in the centre by either matching the colour, shape or
number (of shapes). For example, a player may put a card with 4 red circles on a card with
2 red squares (colour is matched), or a card with 3 green diamonds on a card with 3 blue
circles (number is matched). When a player places a card in the centre, it replaces the one
it is on top of as one of the two cards that must be matched.
A player can pick up the next card from their pile whenever they have less than 3 cards in
their hand. The winner is the first player to put down all 29 of their cards. If both players
reach a point where they are not able to put down any more cards, the game is a draw.
Write a Java program to simulate the game of Speed. Each player must be implemented
as a thread and Peterson’s algorithm must be used where mutual exclusion is required.
(You should not use locks, semaphores, or the synchronized or wait/notify capabilities
of Java objects in this assignment.1
) The program should use the provided class Card.java
本网站支持淘宝 支付宝 微信支付 paypal等等交易。如果不放心可以用淘宝交易！
E-mail: [email protected] 微信:itcsdx