только обновляет поля EHR в верхнем кадре, требование 1 выполняется для n + 1. Точность ISR(j) может быть выражена подобно случаю n = 0, за исключением равенства
IS.TOP.EHRb = is.top.ehrc-1 .
Однако, это равенство действительно из-за уравнения 5.2.
|
Лемма 5.4 |
Пусть механизм прерывания подчиняется программным ограничениям. Тогда выполнение правильно вложенных процедур обработки прерываний не прерывается.
|
ДОКАЗАТЕЛЬСТВО |
Мы выполним за три шага:
1. save никогда не прерывается: Согласно программному ограничению 2, коды save и restore избегают любого немаскируемого внутреннего прерывания. Сброс – единственное немаскируемое внешнее прерывание, но нас интересует только не прерывающееся выполнение. Таким образом, SAVE и RESTORE могут прерываться только маскируемыми прерываниями.
Если команда Ii вызывает прерывание, все маски очищаются, т.е., SRi = 0, и инициализируется переход на ISR: JISRi= 1. В коде save маски обновляются только последней командой. Так как новые маски применяются к более поздним командам, save также не может быть прервано маскируемыми прерываниями.
2. Код restore избегает немаскируемых прерываний, и только последняя команда обновляет регистр состояний. Таким образом, restore не может быть прервано, если оно начинается с SR = 0. Последняя команда любого non-aborting обработчика прерываний – специальное перемещение
SR := GPR[0] = 0.
Если это специальное перемещение не прерывается, тогда restore также не прерывается.
3. Пусть код restore включает команды R1 ... RS. Обратите внимание, что конструкция процедуры обработки прерываний каждого примера ISRстартует с save и – в случае если не прерывается - она выполняет позже точно одну первую команду R1 из последовательности restore. Поэтому, в выполняющейся процедурой обработки прерываний последовательности saves (которая никогда не прерывается) и команды R1формируют начальный сегмент соответствующей скобочной структуры.
В не прерывающемся выполнении, мы обозначим через Rn1энное нахождение R1. Мы докажем индукцией по n, что до Rn1
• кодовый сегмент restore всегда стартует с SR = 0 (следовательно, он не прерывается),
|
QED |
• кодовые сегменты save и restore формируют начальную последовательность соответствующей скобочной структуры, и
• парные скобки принадлежат выполнению некоторого ISR(j).
Для n = 1 save должно быть левее первого R1 . Рассмотрим сначала такое save слева от R11 . Тогда, эти save и R11принадлежат к непрерывному примеру ISR(j). Таким образом, R11стартует с SR = 0 и первый RESTORE является непрерывным.
Для шага индукции рассмотрим R1n+1. Есть nкоманд Ri1слева. По индукционной гипотезе кодовые сегменты save и restore до Rn1 формируют начальную последовательность соответствующей скобочной структуры с парными скобками, принадлежащими выполнению этого ISR(j). По лемме 5.3, эти выполнения точны. Так как последовательность SAVES и R1sформируют начальный сегмент скобочной структуры, мы можем объединить R1n+1 с предшествующей save кодовой последовательностью L . Пусть H' – последовательность команд между L и R1n+1. Создадим Hиз H' отменив все выполнения соответствующего ISR(j). Поскольку эти выполнения точны, мы имеем в течении Hпостоянный уровень прерываний
il = i,
таким образом, обработчик H(i) выполняется в течение H.
Пусть ISR(jn) означает образец ISR, который принадлежит R1n. Тогда команда R1n+1непосредственно предшествует
(a) специальному перемещению I с SR := 0, или
(b) специальному перемещению I сопровождаемому ISR(jn).
Первый случай легкий (смотри n = 1). Во втором случае, ISR(jn) прерывает специальное перемещение, и прерывание jnимеет тип continue. Из-за точности ISR(jn), R1n+1начинается с маской SRum= 0, и (n+ l) блок restore не прерывается.
|
Лемма 5.5 |
Приоритетный критерий. Для допустимых процедур обработки прерываний это означает:
1. В течении выполнения ISR(j), маскируемые прерывания i при i>= j маскируются все время.
2. ISR(j) может прерываться только прерываниями i < j высшего приоритета.
Уважаемый посетитель!
Чтобы распечатать файл, скачайте его (в формате Word).
Ссылка на скачивание - внизу страницы.