SOP wyk nr 11-Slajd10: Różnice pomiędzy wersjami
Nie podano opisu zmian |
Nie podano opisu zmian |
||
| Linia 4: | Linia 4: | ||
Przeplot jest takim globalnym uporządkowaniem akcji w systemie, które zachowuje porządek wynikający z programu każdego ze współbieżnych procesów. Używając zależności teoriomnogościowych, można stwierdzić, że | Przeplot jest takim globalnym uporządkowaniem akcji w systemie, które zachowuje porządek wynikający z programu każdego ze współbieżnych procesów. Używając zależności teoriomnogościowych, można stwierdzić, że Y<sub>1≤x<sub>n</sub></sub>→<sub>i</sub>⊆→ lub dokładniej, że relacja → jest liniowym rozszerzeniem przechodniego domknięcia sumy mnogościowej Y<sub>1≤x<sub>n</sub></sub>. | ||
Przeplot może być analizowany w kontekście zrealizowanego już przetwarzania, a może być rozważany potencjalnie, jako ciąg dopuszczalnych zdarzeń i wynikających z nich stanów, na potrzeby weryfikacji poprawności lub innych własności. W tym drugim przypadku, uwzględniając niedeterminizm, należałoby raczej mówić o pewnym zbiorze możliwych przeplotów, czyli różnych uporządkowaniach tego samego lub zbliżonego zbioru zdarzeń. Różnice w samym zbiorze zdarzeń mogą wynikać z faktu, że w zależności od stanu przetwarzania, przebieg sterowania w poszczególnych procesach może być nieco inny, w związku z czym pewne instrukcje mogą zostać pominięte. | Przeplot może być analizowany w kontekście zrealizowanego już przetwarzania, a może być rozważany potencjalnie, jako ciąg dopuszczalnych zdarzeń i wynikających z nich stanów, na potrzeby weryfikacji poprawności lub innych własności. W tym drugim przypadku, uwzględniając niedeterminizm, należałoby raczej mówić o pewnym zbiorze możliwych przeplotów, czyli różnych uporządkowaniach tego samego lub zbliżonego zbioru zdarzeń. Różnice w samym zbiorze zdarzeń mogą wynikać z faktu, że w zależności od stanu przetwarzania, przebieg sterowania w poszczególnych procesach może być nieco inny, w związku z czym pewne instrukcje mogą zostać pominięte. | ||
Aktualna wersja na dzień 10:44, 16 sie 2006
Przeplot i osiągalność stanu
Przeplot jest takim globalnym uporządkowaniem akcji w systemie, które zachowuje porządek wynikający z programu każdego ze współbieżnych procesów. Używając zależności teoriomnogościowych, można stwierdzić, że Y1≤xn→i⊆→ lub dokładniej, że relacja → jest liniowym rozszerzeniem przechodniego domknięcia sumy mnogościowej Y1≤xn.
Przeplot może być analizowany w kontekście zrealizowanego już przetwarzania, a może być rozważany potencjalnie, jako ciąg dopuszczalnych zdarzeń i wynikających z nich stanów, na potrzeby weryfikacji poprawności lub innych własności. W tym drugim przypadku, uwzględniając niedeterminizm, należałoby raczej mówić o pewnym zbiorze możliwych przeplotów, czyli różnych uporządkowaniach tego samego lub zbliżonego zbioru zdarzeń. Różnice w samym zbiorze zdarzeń mogą wynikać z faktu, że w zależności od stanu przetwarzania, przebieg sterowania w poszczególnych procesach może być nieco inny, w związku z czym pewne instrukcje mogą zostać pominięte.
Z punktu widzenia analizy określonych własności, typu bezpieczeństwo, żywotność, zakleszczenie, istotny jest nie tyle przeplot ile stan systemu, który powstanie w wyniku zajścia zdarzeń w przeplocie. Kluczowe w tym kontekście jest pojęcie osiągalności stanów. Osiągalność jakiegoś stanu z innego stanu zachodzi wówczas, gdy istnieje przeplot, który prowadzi z jednego stanu do drugiego. Wyraża to formalnie definicja rekurencyjna, przedstawiona na slajdzie.
