首页 >
> 详细

Problem 1 (verification)

Three processes share a global variable x, and each process

(named P; in a mixed syntax) performs the following:

int k; /* local variable */

for (k = 0; k < 5; k++) {

LOAD(x); INCREMENT(x); STORE(x);

}

That is, each process executes “x++;” five times, but each

assignment is realized in three steps using its own register.

Now consider the following parallel program:

x = 0;

run P(); run P(); run P();

What is the smallest possible value of x upon program

termination? Make a conjecture and verify that using Spin.

Hints for Problem 1

1. Model the three processes and the main (init) program in

Prolmela

by implementing the behavior of LOAD, INCREMENT, and

STORE using the constructs of Promela.

2. Suppose your conjecture is x==5. Two steps are necessary:

a. Verify that x==5 is a possible outcome upon termination.

This can be done by asserting that, when only one

process (the main process) remains active after three run

P(); x cannot be 5.

The number of active processes can be obtained by the

_nr_pr special variable or by counting them explicitly.

b. Verify that x<5 is not a possible outcome upon termination.

52

Problem 2 (verification) 53

Two global int variables, x and y, are initialized to 10 and 0.

Two threads execute the following statements (in mixed syntax):

Thread 1: while (x != y) {x = x - 1; y = y + 1;}

Thread 2: await (x == y); atomic{x = 8; y = 2;}

Like in Promela, each assignment is an atomic action. Write a

Promela model that captures the behavior of this system and

1. Use Spin to check if both threads always terminate, and to

show what the final values of x and y can be.

2. Explain what happens if the two assignments in Thread 2 are

not done atomically, and confirm your explanation using Spin.

Note: There may (and may not) be two or more final values.

Hints for Problem 2 54

Suppose you think that the possible final values are (𝑥1, 𝑦1)

and 𝑥2, 𝑦2 . Then you need to verify two things:

1. Both (𝑥1, 𝑦1) and 𝑥2, 𝑦2 are possible outcomes.

2. Any pair of values other than (𝑥1, 𝑦1) and 𝑥2, 𝑦2 are

not possible.

Problem 3* (simulation)

Our “Small Set of Integers” program maintains a set of integers

using a linear list of processes. An alternative representation

of sets would use an ordered binary tree of processes in order

to achieve better response to ‘has’ messages.

Write a Promela model of this binary tree

representation, and check if it correctly

responds to a sequence of ‘insert’ and

‘has’ messages.

Note: Testing (rather than verification)

is sufficient for this problem, but make

sure that your test data cover all possible branches.

Note: It is not required to balance the tree.

Problem 4 (verification) 56

A counting semaphore allows N (rather than one) client

processes to enter a critical section at the same time.

Extend our binary semaphore model (Version 2, slide 24)

to a counting semaphore with a general N, where N is given as

a parameter upon process creation.

Then, create a counting semaphore with N=3, run it with five

client processes wanting to enter critical sections infinitely

often, and check that

1. it never lets more than three processes enter the critical

sections, and that

2. it may let three processes enter the critical sections.

Note: You may have to change the algorithm of slide 24.

Problem 5* (verification) 57

The semaphores in the course slides may cause starvation

(i.e., some process cannot enter a critical section in finite time).

To avoid it will require a different design. Design and

implement a counting semaphore that won’t cause starvation.

Then, create a counting semaphore with N=3, run it with five

client processes wanting to enter critical sections infinitely

often, and check that

1. it never lets >3 processes enter the critical sections,

2. it may let three processes enter the critical sections, and

3. a process wanting to enter a critical section will enter it

eventually.

Hint: Consider using a channel with non-zero capacity.

Assignment #1 (1/2)

Solve Problems 1 to 5 (Problems 3 and 5 are optional, but

choose at least one of them). Your report should include:

problem analysis (i.e., how you reached your solutions),

the Promela models you wrote,

execution results (for verification problems, copy and

paste the first dozen or so lines up to “atomic steps”), and

discussions.

Notes:

(1) You must use the verification mode except for Problem 3.

(2) You can add auxiliary variables, expressions, statements,

and processes for the purpose of verification.

(3) To solve each problem, you may run your program(s)

several times using different assertions or parameter values.

联系我们

- QQ：99515681
- 邮箱：99515681@qq.com
- 工作时间：8:00-23:00
- 微信：codinghelp2

- 代做r语言编程|代做spss|代写web开发|代做... 2021-05-10
- Data留学生编程代做、代写analysis程序、Sql语言程序调试代做r语 2021-05-10
- 代写31748程序语言、代做programming编程设计、Java，Pyt 2021-05-10
- 代做cis 657编程、代写c/C++程序、C++编程调试帮做haskell 2021-05-10
- Com1005程序代写、代做java编程语言、代写java程序代做留学生pr 2021-05-10
- 代写sit283程序、代做c/C++，Python编程设计、Cs，Java程 2021-05-09
- C++程序代做、代写c++程序、代写program编程语言代做r语言编程|代 2021-05-09
- 代写0ccs0cse编程、代做r，Java，Python程序语言代写web开 2021-05-09
- Comp124编程语言代做、Java程序代做、代写program语言编程代写 2021-05-09
- Comp122编程语言代写、代做java程序语言、Java程序调试帮做has 2021-05-09
- 代做ele00041i 调试java Programming 2021-05-08
- 代做econ 2014-Assignment 1 Managerial... 2021-05-08
- 代写mast90044-Assignment 1 Thinking An... 2021-05-08
- 代做cs310-Assignment 2 Hash Tables 2021-05-08
- 代写5pm 调试java编程、Java编程代写 2021-05-08
- 代写cs544 Final Exam Preparation Guide... 2021-05-08
- 代做infs7450 Social Media Analytics 2021-05-08
- 代做iab201-Assignment 1 Information Mo... 2021-05-08
- 代写gu4265/Gr5265 Midterm Exam 2021-05-08
- 代做engn3213/6213 Finite State Machine... 2021-05-08