BD-2st-1.2-w08.tresc-1.1-Slajd29
Twierdzenie o konfliktowej uszeregowalności
Możemy obecnie, korzystając z grafu konfliktowej uszeregowalności sformułować twierdzenie, pozwalające w sposób algorytmiczny weryfikować, czy dana realizacja współbieżna jest poprawna, tj. konfliktowo-uszeregowalna. Realizacja r(TAU ) zbioru transakcji T jest konfliktowo-uszeregowalna wtedy i tylko wtedy, gdy jej graf konfliktowej uszeregowalności CSRG(r(TAU )) jest acykliczny.
Poprawność powyższego twierdzenia wynika bezpośrednio z własności spójności transakcji. Zgodnie z własnością spójności, każda transakcja transformuje bazę danych z jednego stanu spójnego do innego stanu spójnego. Stąd wynika, że każda realizacja sekwencyjna zbioru transakcji zachowuje spójność bazy danych, gdyż jest ona sekwencją transformacji odwzorowujących bazę danych z jednego do innego stanu spójnego. Z definicji grafu konfliktowej uszeregowalności wynika, że graf ten, dla dowolnej realizacji sekwencyjnej, musi być acykliczny. Z definicji kryterium konfliktowej uszeregowalności wynika, że dowolna realizacja współbieżna jest poprawna, jeżeli jest ona równoważna dowolnej realizacji sekwencyjnego tego samego zbioru transakcji. Z definicji równoważności realizacji wynika, że graf konfliktowej uszeregowalności realizacji współbieżnej musi być również acykliczny, jeżeli realizacja ta jest konfliktowo-uszeregowalna. Co kończy skrótowy dowód poprawności podanego twierdzenia.
