本次Java代写是使用演绎技术证明Peterson算法的正确性

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

student number.

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).

1

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

**程序代写代做C/C++/JAVA/安卓/PYTHON/留学生/PHP/APP开发/MATLAB**

本网站支持淘宝 支付宝 微信支付 paypal等等交易。如果不放心可以用淘宝交易！

**E-mail:** [email protected] **微信:**itcsdx

如果您使用手机请先保存二维码，微信识别。如果用电脑，直接掏出手机果断扫描。