If below is the solution to the bounded buffer problem with 1 producer, 1 consum

Question

If below is the solution to the bounded buffer problem with 1 producer, 1 consumer, and 1 buffer X, what would the solution be to the same problem except with 1 producer, 2 consumers, and 2 buffers? It is okay if each consumer consumes only from 1 of the 2 buffers, but the producer must produce to both buffers.

X::
buffer: (0..9) portion;

in,out: integer; in := 0; out := 0;
comment 0 <= out <= in <= out + 10;

*[in < out + 10; producer?buffer(in mod 10) ->
     in := in + 1;

out < in; consumer?more() ->
     consumer!buffer(out mod 10);
     out := out + 1;
]

Explanation / Answer

let the solution be Y

Y::
buffer1: (0..9) portion;
buffer2: (0..9) portion;

in,out: integer; in := 0; out := 0;
comment 0 <= out <= in <= out+10;

*[in < out + 10; producer?buffer1(in mod 10) ->
     in := in + 1;

*[in < out + 10; producer?buffer2(in mod 10) ->
     in := in + 1;

[] out < in; consumer1?more() ->
     consumer!buffer1(out mod 10); out := out + 1;

[] out < in; consumer2?more() ->
     consumer!buffer2(out mod 10); out := out + 1;

Related Questions

Navigate

• Browse (All)
• Browse I
• Subjects

Integrity-first tutoring: explanations and feedback only — we do not complete graded work. Learn more.