Q : FIFOQ : FIFO
3.4. Stan modelu
0 1 2 3 Tx-3 Tx-2 Tx-1 Tx running ready am(Xi) ready SysTick SysTick running 2Tx-32Tx-22Tx-1 2Tx 2Tx+1 Tx+1 Tx+2 agent Xi
zablokowana część instrukcji, przeniesiona do następnego trybu X (running)
czas
Tb' Tb'
ci(A) = sft(n)
Rysunek 3.9: Granulacja instrukcji z punktu widzenia domeny czasu w warstwie systemowej α1 FPPS
Istniej ˛a dwie mo˙zliwo´sci, okre´slaj ˛ace sposób w jaki mo˙zna doko´nczy´c instrukcj˛e: opó´zni´c konsekwencje przerwania systemowego (potencjalne wywłaszczenie agenta Xi) o czas T00
b i doko´nczy´c instrukcj˛e lub przenie´s´c doko´nczenie instrukcji do momentu, w którym agent Xi znów b˛edzie w trybie running. W tej rozprawie doktorskiej zało˙zono, ˙ze przerwanie systemowe SysTick nie mo˙zne zosta´c opó´znione i przerwana instrukcja zostaje doko´nczona po ponownym przej˛eciu zasobów procesora przez agenta Xi.
W ten sposób granulacja instrukcji jest ustalana na poziomie pojedynczej jednostki czasu, a nie czasu wykonywania całej instrukcji. W rezultacie tego zało˙zenia analiza warstwy systemowej α1
FPPS musi
uwzgl˛ednia´c stany agentów, w których poszczególne instrukcje nie zostały uko´nczone. Informacja o tym, ˙ze dana instrukcja potrzebuje jeszcze n jednostek czasu do uko´nczenia, zawarta jest na li´scie kontekstowej agenta w postaci wpisu sft(n).
Rozwa˙zmy przykład pokazany na rysunku 3.10. Algorytm szereguj ˛acy warstwy systemowej α1 FPPS
wywłaszcza agenta aktywnego A z powodu przerwania systemowego SysTick, które wyst ˛apiło w momencie czasowym T = 100. Instrukcja o czasie trwania Tbnadal potrzebuje dwóch jednostek czasu do uko´nczenia. W my´sl przyj˛etych zasad w kwestii granulacji instrukcji, doko´nczenie procesowania zostaje przeniesione do czasu, a˙z agent A znów b˛edzie w trybie running. W rozwa˙zanym przykładzie dzieje si˛e to w momencie czasowym T = 200. Do tego czasu na li´scie kontekstowej agenta A widnieje wpis sft(2) informuj ˛acy o tym, ˙ze instrukcja nie została zako´nczona i potrzebuje ci ˛agle dwóch jednostek czasu.
3.4. Stan modelu
W celu opisania bie˙z ˛acego stanu dla danego modelu systemu współbie˙znego potrzebne s ˛a stany wszyst-kich agentów zdefiniowanych w modelu oraz stan bie˙z ˛acy dwuwymiarowej kolejki FIFO.
3.4. Stan modelu 40 0 1 2 3 97 98 99 100 101 102 103 running ready am(A) 197 198 199 200 ready 201 agent A(1) SysTick SysTick running 202 czas
zablokowana część instrukcji, przeniesiona do następnego trybu X (running)
ci(A) = sft(2) ci(A) = sft(5)
Rysunek 3.10: Przykład granulacji instrukcji z punktu widzenia domeny czasu w warstwie systemowej α1FPPS
Definicja 3.3. Niech dany b˛edzie model niehierarchiczny A = (D, B, α1
FPPS), gdzie D = (A, C, σ) i A = {X1, . . . , Xn}. Niech Q b˛edzie uporz ˛adkowan ˛a dwuwymiarow ˛a kolejk ˛a FIFO dla warstwy systemowej alpha1FPPS oraz niech t oznacza liczb˛e jednostek czasu do ponownego wywołania algorytmu szereguj ˛acego.
Stan modelu A jest krotk ˛a:
S = (S(X1), . . . , S(Xn), (Q, t)). (3.6) Dla ka˙zdego stanu modelu S i ka˙zdego agenta X ∈ AAzachowane s ˛a nast˛epuj ˛ace warunki:
critical ∈ ci(X) ⇒ ∀Y ∈AA\{X}am(Y ) 6= X, (3.7)
|{X ∈ AA: am(X) = X}| ≤ 1. (3.8)
Zdefiniowanie stanu pocz ˛atkowego modelu wymaga okre´slenia w jaki sposób uporz ˛adkowana jest ko-lejka Q w stanie pocz ˛atkowym, tj. w jakiej kolejno´sci s ˛a wstawiane do kolejki agenty aktywne Xii Xj, w przypadku, gdy maj ˛a taki sam priorytet. Przyj˛ecie zało˙zenia, ˙ze rozwa˙zane s ˛a wszystkie mo˙zliwe warianty w ramach uszeregowania agentów w poszczególnych wierszach kolejki Q, prowadzi do sytuacji, w której uzyskuje si˛e wiele mo˙zliwych stanów pocz ˛atkowych. Z drugiej strony niektóre narz˛edzia do weryfikacji modelowej np. CADP wymagaj ˛a, aby stan pocz ˛atkowy modelu był okre´slony jednoznacznie. Z tych prak-tycznych wzgl˛edów przyj˛eto, ˙ze kompilator umieszcza agenty o tym samym priorytecie w kolejno´sci ich definiowania w kodzie modelu. U˙zytkownik mo˙ze zmodyfikowa´c odpowiedni fragment kodu w Haskellu i okre´sli´c inny stan pocz ˛atkowy. Oczywi´scie zastosowanie ró˙znych priorytetów eliminuje ten problem. Definicja 3.4. Niech dany b˛edzie model niehierarchiczny A = (D, B, α1
FPPS), gdzie D = (A, C, σ) i A = {X1, . . . , Xn}. Niech Q b˛edzie uporz ˛adkowan ˛a dwuwymiarow ˛a kolejk ˛a FIFO dla warstwy systemowej J. Baniewicz Metody formalnej analizy systemów wbudowanych czasu rzeczywistego
3.5. Podsumowanie 41
alpha1
FPPS oraz t niech oznacza liczb˛e jednostek czasu do ponownego wywołania algorytmu szereguj ˛acego. Stan pocz ˛atkowy modelu A jest krotk ˛a:
S0 = (S0(X1), . . . , S0(Xn), (Q0, t)) (3.9) której zawarto´s´c okre´slana jest przez nast˛epuj ˛acy algorytm:
1. amS(X) = Rdla agenta X ∈ AAtakiego, ˙ze σ(X) = T rue;
2. amS(X) = Idla ka˙zdego agenta X ∈ AAtakiego, ˙ze σ(X) = F alse; 3. amS(X) = Wdla ka˙zdego agenta X ∈ AP;
4. pc(X) = 1 dla ka˙zdego agenta X ∈ AAb˛ed ˛acego w trybie ready; 5. pc(X) = 0 dla ka˙zdego agenta X ∈ AAb˛ed ˛acego w trybie init; 6. pc(X) = 0 dla ka˙zdego agenta X ∈ AP;
7. ci(X) = [ ] dla ka˙zdego agenta X ∈ AA;
8. Dla ka˙zdego agenta X ∈ AP, ci(X) zawiera nazwy wszystkich dost˛epnych procedur tego agenta X razem z kierunkiem przesyłania parametrów, np. in(a), out(b) itp.;
9. Dla ka˙zdego agenta X ∈ A, pv(X) zawiera warto´sci pocz ˛atkowe parametrów tego agenta;
10. Wszystkie agenty b˛ed ˛ace w trybie ready umieszczane s ˛a w kolejce Q zgodnie z warto´sci ˛a ich prio-rytetów. O pozycji agentów w poszczególnych wierszach decyduje u˙zytkownik lub przyjmowany jest układ domy´slnie generowany przez kompilator.
11. Agent Xrwyznaczony zgodnie ze wzorem (3.3) usuwany jest z kolejki Q, a jego tryb ustawiany jest na warto´s´c running.
3.5. Podsumowanie
W niniejszym rozdziale skupiono si˛e nad zagadnieniami zwi ˛azanymi z formalnym opisem stanu mo-delu, który wykorzystuje warstw˛e systemow ˛a α1
FPPS. Przeniesienie semantyki j˛ezyka Alvis na systemy jednoprocesorowe wymagało wprowadzenia istotnych zmian w opisie stanów agentów i modeli, w porów-naniu z definicjami przedstawionymi w pracy [52]. Poza adaptacj ˛a wybranych poj˛e´c (np. tryb agenta, lista kontekstowa) do potrzeb warstwy systemowej α1
FPPS, przedstawiono koncepcj˛e dwuwymiarowej kolejki szereguj ˛acej agenty oczekuj ˛ace na przydział procesora. Zdefiniowana kolejka Q stanowi istotne rozszerze-nie opisu stanu modelu, wprowadzone dla warstwy systemowej α1
FPPS. Do wkładu własnego autora rozprawy nale˙zy zaliczy´c:
• Opracowanie koncepcji warstwy systemowej α1
FPPS, w tym przedstawienie głównych zało˙ze´n algo-rytmu szereguj ˛acego, sposobu kolejkowania i wywłaszczania agentów przy stałym okresie zgłaszania przerwania systemowego.
3.5. Podsumowanie 42
• Definicj˛e dwuwymiarowej kolejki FIFO do szeregowania agentów i zarz ˛adzania nimi w przypadku promocji jednego z nich do trybu running.
• Opracowanie metody ustalania stanu pocz ˛atkowego dla modeli z warstw ˛a systemow ˛a α1 FPPS.