Assignment Two 一 25%

Concurrency:  Theory and Practice 一 CSSE7610 一 Semester 2, 2025

Due: 4pm on Friday October 24 (Week 12)

Summary

The objective of this assignment is to explore a concurrent card game.  As part of this assignment, you will design concurrent algorithms, prove and validate different properties both manually and mechanically via TLA+.  Then, you will implement the card game in Java.

Scary Warnings

You should read this specification in its entirety. There are some aspects that will catch you out if not. For example, Section 4 has some critical information on expectations for referencing your code, details on some required files you must submit, and a list of penalties that can be applied to your assignment solution. Please be aware.

0 Speed

“Speed” is a real-time card game (as opposed to a turn-based game) where players (processors) interact via a shared state: four piles of cards.

Setup. Create a hand containing 5 cards for each of two players P and Q, and call these handP  and handQ.  Create a private deck of 15 cards for each player, and call these drawP and drawQ. Create two initial discard decks; a left and a right deck, and call these discardL and discardR . Each discard deck begins with just one card. Create two pickup decks of 5 cards on the left and right, and call these pickupL  and pickupR .

Assume pick(n) randomly draws n cards that are not currently in use.

handP  ← pick(5);       handQ  ← pick(5);        drawP  ← pick(15);    drawQ  ← pick(15);

discardL  ← pick(1);   discardR  ← pick(1);    pickupL  ← pick(5);   pickupR  ← pick(5);

Objective. The first player to empty both their hand and draw pile wins.

Rules.

1. If a player has a card in their hand with a value one greater or less than the top of either discard pile (discardL  or discardR ), they may transfer that card to that pile.

2. If a player has less than 5 cards in their hand, they must draw from their respective draw pile (drawP  or drawQ ).

3. If both players can not make one of the above moves, the players simultaneously draw a card from different pickup piles and play the card on the corresponding discard deck.

discardL.push(pickupL.pop())  ||  discardR.push(pickupR.pop())

4. Once the pickup piles are depleted, the discard and pickup piles are shuffled and re-dealt such that the discard piles have 1 card each and the pickup piles have an even (if odd, one pile will have exactly one more than the other) split of the remaining cards.

Tasks

In this assignment you will:

1. Design a monitor to enable safe concurrent game play.

a. Prove safety and liveness properties of the monitor.

b. Provide an example of live locking.

2. Model the monitor in TLA+.

3. Implement a Java simulation of the game.

a. Implement a blocking monitor based Java implementation.

b. (Bonus) Implement a non-blocking Java implementation.

1 Speed Monitor

Algorithm S below contains a partial implementation of a game of speed.

You can assume that the function canPlay(card, top) exists and returns true if card can be played on top of the card top.

Task 1. Complete the implementation of the Speed monitor according to the rules above.

Task 2. We want to ensure that the following two properties hold:

Safety: The sequence of cards in each discard deck is valid (according to canPlay(card, top)). Liveness: The player will always eventually make a move while the game is not finished.

Express these properties as formulas and prove that they hold for your monitor specification.

Task 3. Provide an example scenario where a live lock may occur.

Deliverable: A file speed.pdf containing your the completed Speed monitor, a proof of the above properties, and your livelock scenario. Include your name and student number at the top.

2 TLA+ Specification

Translate your monitor specification into a PlusCal algorithm in TLA+. You may use the provided macros and procedures to express your algorithm. Direct translation will cause a state space explosion. Your specification must model the game play more abstractly. Some examples of abstractions you can make include (but are not limited to):

1. Model only one discard and one pickup pile.

2. Decide non-deterministically a) whether a card can be played and b) which card to play. Do not model the card playing rules of the game. You may find the TLA+ either and with constructs useful.

3. You may reduce the size of the decks.

Use your specification to show that the algorithm

1. does not deadlock,

2. preserves mutual exclusion within the monitor, and

3. that both processes progress.

You may make other simplifications to the specification as long as the behaviour relevant to the desired properties above are preserved.

Deliverable:  A file speed .tla containing the TLA+ specification.  The algorithm must be specified by Spec, and safety and liveness properties should be specified by Safety and Liveness respectively. You should use commenting to describe the abstraction made to the algorithm and justify that it is safe. Again, ensure your name and student number are at the top.

3 Speed in Java

Implement your algorithm for the speed card game in Java.  You should first implement the algorithm using the Java monitor pattern.  Your Java implementation should match your algorithm from Part 1 as closely as possible while maintaining correctness using Java’s monitor implementation.

Your implementation must implement the provided ISpeed interface:

To record that a game event has occurred, you must call the appropriate method on the EventListener interface.

3.1    Super Speed (Bonus)

A monitor implementation of speed requires synchronization; one process must obtain a lock before playing a card. This is a blocking solution. Implement a non-blocking implementation of speed, called super speed, that preserves the correctness.  Note that only playing cards from player hands to the discard pile should be non-blocking. Determining when to flip the pickup piles into the discard pile requires synchronization but this must be implemented without using a synchronized method.

4 Assessment

This section briefly describes how your assignment will be assessed.

Mark Allocation

Marks will be provided based on the correctness and readability of your answers to all questions.

Part One (8 marks)

◆   Monitor implementation                                                                                         (4 marks)

◆   Proof of safety                                                                                                          (1 mark)

◆   Proof of liveness                                                                                                     (2 mark)

◆   Livelock scenario                                                                                                    (1 mark)

Part Two (9 marks)

◆  TLA+ specification                                                                                                 (3 marks)

◆  Abstraction of algorithm                                                                                        (2 marks)

◆   Specification of non-determinism                                                                         (2 marks)

◆   Proof of mutual exclusion                                                                                        (1 mark)

◆   Proof of progression                                                                                               (1 mark)

Part Three (8 marks + 4 bonus)

◆  Java speed implementation                                                                                   (8 marks)

◆  Java super speed implementation                                                               (4 bonus marks)

Penalties Penalties will be computed and removed from your overall final mark as follows:

◆   If your code does not adhere to good style principles (such as those shown in the guide provided on the Blackboard (Course  Resources  >  Java  Resources), you will lose 2 marks;

◆   If your submission does not include the statement .txt file, or if the statement is empty, you will lose 25 marks, no exceptions – see the instructions regarding the statement below.

Plagiarism and Generative AI

If you want to actually learn something in this course, our recommendation is that you avoid using Generative AI tools: You need to think about what you are doing, and why, in order to put the theory (what we talk about in the lectures and tutorials) into practical knowledge that you can use, and this is often what makes things “click” when learning.  Mindlessly lifting code from an AI engine won’t teach you how to solve problems, and if you’re not caught here, you’ll be caught soon enough by prospective employers.

If you are still tempted, note that we will be running your assignments through sophistic- ated software similarity checking systems against a number of samples including including your classmates and our own solutions (including a number that have been developed with AI assistance). If we believe you may have used AI extensively in your solution, you may be called in for an interview to walk through your code.  Note also that the final exam may contain questions or scenarios derived from those presented in the assignment work, so cheating could weaken your chances of successfully passing the exam.

AI Statement As part of your submission, you must submit a text file statement .txt that provides attribution to any sources or tools used to help you with your assignment, including any prompts provided to AI tooling. If you did not use any such tooling, you can make a statement outlining that fact. Failing to submit this file, or submitting an empty file, will result in a 25 mark penalty.

Please refer to the referencing guide for assessments located in the “Assessment” tab on Blackboard for more information.

Interviews We will be conducting assignment interviews, where a subset of students will be invited to walk through their assignment submission with a member of staff. Your final assignment score will be weighted according to your demonstrated understanding of your submission, where the weight will be assigned in the range [0.0, 1.0]. Note that students who are not selected for interviews will have this weight set to 1.0 by default. For example:

◆   Student A scores 18 marks. They are not interviewed. Their final score remains at 18 marks.

◆   Student B scores 12 marks.  They are interviewed, and they are judged to have a full understanding of their submission giving them a weighting of 1.0, resulting in 12 marks.

◆   Student C scores 19 marks. They are interviewed, and they are judged to have a mostly complete understanding of their submission, but are lacking understanding of some parts of their algorithms, giving them a weighting of 0.75.  This means their final mark is 0.75 × 19 = 14.25.

Students may be selected for an interview according to their reported AI usage (or lack thereof) as noted in their statement file, their assignment similarity with other students and/or AI generated solutions, their mark as compared to their past performance, or totally randomly.

Submission Information

You need to submit your solution to Gradescope under the Assignment 2 link  in your dashboard. The easiest way to submit your solution is to submit a  .zip file. As described earlier, your zip file should contain the following files:

◆   speed.pdf – Part 1.

◆   speed .tla – Part 2.

◆   src/ – A subdirectory containing all code and the README for Part 3.

◆   statement .txt – The AI/reference statement.