Детальный проект конвейерного RISC процессора (Глава 5 "Обработка прерываний"), страница 8

Согласно лемме 5.4, коды save и RESTORE могут прерываться только сбросом. Таким образом, мы сосредотачиваемся на обработчиках прерываний. Для любого немаскируемого прерывания j < 6 второе требование следует непосредственно из ограничения 2. Для маскируемых прерываний j >= 6 мы докажем требования индукцией по числу n прерываний которые прерывают обработчик H(j).

• n= 0: ISR всегда начинается с SR = 0, из-за сигнала JISR. ISR модифицирует маски только специальным перемещением movi2s или командой rfe. Так как rfe используется только как последняя команда ISR (ограничение 2), у нее нет влияния на маски используемые самой ISR. В случае специального перемещения SR:= R, бит R[i] должен быть нулем для любых i >= j.Таким образом, маскируемые прерывания маскируются правильно. Из-за определения причины маскируемых прерываний команды I_l

и определения уровня прерываний

il_l = min{j' | MCA[j']_l = 1},

ISR(j) не может быть прервано маскируемыми прерываниями j' >= j, и требование выполняется.

• n > 0: Обработчик H(j) прерывается nраз, и коды save и restore формируют соответствующую скобочную структуру. Таким образом, последовательность команд ISR(j) имеет следующую форму

Save... ISR( j₁ ) ... ISR( j_m ) ... Restore,

для любых m <= n. Команды, которые принадлежат коду обработчика H(j) не размаскируют прерывания j’ при j' <= j. Из-за точности ISR, любые ISR( j_r ) возвращают маски SRпоставленные этому регистру ESR. Индукцией по mтогда следует, что прерывание j_r имеет более высокий приоритет, чем j,т.е., j_r < j.

Так как любое ISR( j_r ) прерывается самое большее n - 1 раз, применима индукционная гипотеза. ISR( j_r ) сохраняет все прерывания j' с j' >= j_r маскируемыми, в особенности, с j' >= j.

Теорема 5.2 и лемма 5.5 подразумевают:

Не прерывающееся выполнения допустимой процедуры обработки прерываний – совершенно вложенные.

Пусть LHR– не прерывающееся выполнение ISR(j), где L – сохраняющая последовательность и R– восстанавливающая последовательность. По теореме 5.2, последовательности saves и restores в LHR– начальные сегменты скобочной структуры. Если скобки Lи R- парные, тогда последовательности save и restore в Hформируют скобочную структуру. Следовательно, скобки в LHRформируют скобочную структуру и LHR– совершенно вложен.

Предположим, что Rпарен с левой скобкой L' правее L:

Тогда по лемме 5.5, уровень прерывания непосредственно перед L' – больше чем  j, и LHR– не непрерывающаяся последовательность.

Согласно лемме 5.5, ISR прерывания j > 0 может быть прервано только прерыванием более высокого приоритета. Таким образом, может быть самое большее один кадр на стеке IS для каждого уровня прерываний j > 0. Сброс может прервать даже ISR(0). Однако, при сбросе ISR не размещает новый кадр, стек IS вместо этого является очищенным. Следовательно, размер стека прерываний IS ограничен; ISR использует самое большее 32 кадра.

Подобно многим программным протоколам, для механизма прерываний желательна справедливость. В этом контексте справедливость означает, что обрабатывается каждое прерывание. Из-за чисто приоритетной схемы это не может всегда достигаться. Рассмотрим случай, когда сигналы событий двух внешних прерываний ev[15] и ev[17] становятся активными в тоже время, когда внешнее прерывание ev[16] происходит всякий раз, когда покидаем ISR(15) и наоборот. При этих условиях, прерывание 17 обламывается прерываниями 15 и 16. Таким образом, справедливость и чисто приоритетная схема не идут вместе. Тем не менее, по крайней мере хотелось бы гарантировать, что ни одно внутреннее прерывание не потеряется.

Законченость Пусть механизм прерываний подчиняется программным требованиям. Каждое внутреннее прерывание j которое происходит в команде I_i и которое не маскируется, получает обслуживание в команде I_i+1 , или команда I_i повторяется после ISR , который начинается с команды I_i+1 .