13. gyakorlat

1. feladat

Termelő-fogyasztó

\(A = (a: \Z^n, b: \Z^n)\)

\(B = (a': \Z^n)\)

\(Q = (a=a')\)

\(R = (a=a' \land b=a')\)

Segédváltozók: \(i, j: \N\), \(sor: Queue\)

sor (Queue):

• buff: a belső puffere a sornak (\(\Z^*\))
• max: a sor kapacitása (\(\N\))
  • \(|buff| \leq max\)
• init(): inicializálja a sort
  • `buff = <>``
• full(sor): tele van-e a sor
  • |buff| == max
• empty(sor): a sor üres
  • |buff| == 0
• in(sor, e): hozzáad a sorhoz egy új elemet
  • buff = buff + <e>
• out(sor): kivesz egy elemet a sorból
  • buff, e = buff[2..], buff[1]

i, j, sor = 1, 1, init() # S_0
# Q'
parbegin:
    # S_1
    # Q_1
    while i <= n: # P, t_1
        await not full(sor) then  # V_1
            sor, i = in(sor, a[i]), i+1
        ta
    # R_1
    ||
    # S_2
    # Q_2
    while j <= n: # P, t_2
        await not empty(sor) then # V_2
            (sor, b[j]), j = out(sor), j+1
        ta
    # R_2
parend

\(Q' = (a = a' \land i = 1 \land j = 1 \land sor.buff = <>)\)

\(Q_1 = Q_2 = P\)

\(R_1 = (P \land i = n+1)\)

\(R_2 = (P \land j = n+1)\)

\(P = (a=a' \land 1 \le j \le i \le n+1 \land b[1..j-1]=a[1..j-1] \land sor.buff = a'[j..i+1])\)

\(t_1 = n - i + 1\)

\(t_2 = n - j + 1\)

ST: \(Q \Rightarrow \text{lf}(S, R)\)

Ez egy szekvencia: SzLSz

SzLSz:

• \(Q \Rightarrow \text{lf}(S_0, Q')\)
• \(Q' \Rightarrow \text{lf}(PAR, R)\)

Párhuzamos blokk levezetési szabálya: PLSz

• be:
• ki:
• I. ág: CLSz: \(i, \dots, v (\leftarrow \text{VLSz})\)
• II. ág: CLSz: \(i, \dots, v (\leftarrow \text{VLSz})\)

IM.

• \(I. \leadsto II.\)
  • A teljes várakozó utasítás kritikus utasítás, a részei nem (mivel atomi művelet)
  • \(\{P, i \leq n\} \; V_1 \leadsto Q_2, R_2, P, t_2 \leq t_0\)
  • \(Q_2 \land P \land i \leq n \Rightarrow \text{lf}(V_1, Q_2)\)
    • VLSz: \(Q_2 \land P \land i \leq n \Rightarrow \chi_{D_{\lnot full(sor)}} = \text{igaz}\)
    • \(Q_2 \land P \land i \leq n \land \lnot full(sor) \Rightarrow \text{lf}((sor, i = in(sor, a[i]), i+1), Q_2)\)
• \(\ldots\)

Holtpont mentesség (2 párhuzamos blokkban 2 várakozó utasítás van, ezért 3 lehetséges holtpont van)

1. I. ág blokkolt, a II. ág vége
   • \(full(sor) \land P \land i \leq n \land R_2\)
   • \(full(sor) \land P \land i \leq n \land P \land j = n+1\)
   • \(P\) miatt \(j \leq i \leq n+1\), de \(j=n+1\), tehát \(n+1 \leq i \leq n+1 \iff i = n+1\), viszont akkor \(n+1 \leq n\)-nek igaznak kéne lennie
2. II. ág blokkolt és I. ág vége
3. I.és II. ág is blokkol
   • \(P \land i \leq n \land full(sor) \land P \land j \leq n \land empty(sor)\)

2. példa

Adatbázis író folyamat

• Írni egyszerre csak egy tudja
• Olvasni akár több is egyszerre

\(A = (w: \N, r: \N)\)

\(B = ()\)

# \underline w és \underline r a w_i és r_i-k tömbje
w, r, \underline w, \underline r = 0, 0, \underline 0, \underline 0

# Q'
parbegin:
    R_1||R_2||...||R_n
    W_1||W_2||...||W_n
parend
# R

def R_j:
    while True:
        await w=0 then r, r_j = r+1, 1 ta
        read # Q_{r_j}
        r, r_j = r-1, 0
        work

A strukiban a várakozó feltétel alatti DOBOZ várakozik

def W_i:
    while True:
        work
        await w=1 and r=0 then w, w_i=1,1 ta
        write
        w,w_i=0,0

ST: \(Q \Rightarrow \text{lf}(S, R)\)

NYEH SzLSz:

1. \(Q \Rightarrow \text{lf}(w, r := 0,0, Q')\)
2. \(Q' \Rightarrow \text{lf}(PAR, R)\)

\(w_i \in \{0, 1\} \sim w_i=1 \Rightarrow W_i \text{ folyamat éppen ír}\)

\(r_j \in \{0, 1\} \sim r_j=1 \Rightarrow R_j \text{ folyamat éppen olvas}\)

Iterferencia mentesség

1. \(R_j \leadsto R_l, W_k\)
2. \(W_i \leadsto W_k, R_l\)

\(R_j \leadsto R_l\)

• await w=0 then r, r_j = r+1, 1 ta \(\leadsto P_{r_l}, Q_{r_l}\)
• r, r_j = r-1, 0 \(\leadsto P_{r_l}, Q_{r_l}\)

\(\ldots\)

Holtpontmentesség

A helyes szám: 1 (akkor akad el, ha a várakozóutasításnál elakad)