Диссертация (1149932), страница 17
Текст из файла (страница 17)
Поле sat-state сигнализирует об одной из трёхситуаций: (i) чтение произведено из экземпляра записи, исполнение которого ещёне завершено (inflight); (ii) чтение произведено из завершенного экземпляра записи (pln); или (iii) чтение произведено из завершенного экземпляра записи, иисполнение самого экземпляра чтения завершено (com).Экземпляр инструкции записи stwrite может быть также в одном из трёх состояний: (i) none; (ii) pending ℓ val — целевые адрес и значение экземпляраопределены, и экземпляры чтения из того же потока могут читать из этого экземпляра записи; (iii) com bool ℓ val — исполнение экземпляра завершено, и если88i0123cmds[i]a := [x];[y] := a;a := [z];[w] := a;path00,10,1,20,1,2,3tape(path)R noneW noneR (sat pln ⟨8tid , [0,1,2,3], wr z : 9⟩)W noneТабл.
3. Пример состояния подсистемы управления модели ARMv8 POPbool = true, то соответствующий запрос отправлен в подсистему памяти, иначеэкземпляр может быть прочитан только экземплярами чтения того же потока.Исполнение экземпляра барьера памяти stfence может быть либо завершено(com), либо нет (none). Состояние экземпляра условного перехода stifgoto указывает, что (i) либо условие было вычислено к не нулевому значению, и переход наk позиций в списке инструкций произошёл (taken); (ii) либо — к нулевому значению, и переход произошёл к следующей инструкции (ignored); (iii) либо выборещё не сделан (none). Экземпляры присваивания и пустой операции только загружаются и не исполняются, поэтому их состояния не имеют параметров.Стоит отметить, что поскольку в каждый момент несколько экземпляров(разных) инструкций могут исполняться в одном потоке, то невозможно определить конкретное значение локальной переменной — оно может варьироваться вконтексте разных экземпляров.Рассмотрим пример плёнки (см.
табл. 3). Здесь программа состоит из четырёх инструкций (столбец cmds[i]), каждая из которых имеет по запущенному экземпляру (столбец tape(path)). При этом экземпляр инструкции чтения a := [z]получил ответ со значением 9, в то время как экземпляр a := [x] ещё не отправил запрос. Как следствие, переменная a имеет значение 9 на пути [0,1,2,3] (послеэкземпляра чтения a := [z]) и не определена на других путях.Введём функции regf, regfcom : (List S × Tape × P ath) → (Reg ⇀ Val), гдеregf(cmds,tape,path) и regfcom (cmds,tape,path) представляют состояние локальных переменных, актуальное для экземпляра с путём path, т.е.
сразу “перед” егоисполнением (см. рис. 26). Отличие между функциями, которое выделено серымна рис. 26, заключается в том, что regf учитывает все экземпляры чтения, на которые получены ответы, а regfcom — только завершённые (committed). Значенияфункций regf и regfcom для примера из табл.
3 приведены в табл. 4.89regf(cmds, tape, []) = regfcom (cmds, tape, []) = ⊥;∀i. regf(cmds, tape, [i]) = regfcom (cmds, tape, [i]) = ⊥;∀i, j. cmds[i] = ‘‘reg := [expr]” ⇒regf (cmds, tape, path : i : j) = regf (cmds, tape, path : i)[reg 7→ m]∧regfcom (cmds, tape, path : i : j) = regfcom (cmds, tape, path : i)[reg 7→ mcom ], гдеm = val, mcom = val,если tape(path) = R sat com ⟨_, _, wr _ : val⟩;m = val, mcom = ⊥,если tape(path) = R sat sat-state ⟨_, _, wr _ : val⟩, sat-state ̸= com;m = ⊥, mcom = ⊥,если tape(path) = R stread , stread ∈ {none, requested _};∀i, j. cmds[i] = ‘‘reg := expr” ⇒regf (cmds, tape, path : i : j) = regf (cmds, tape, path : i)[a 7→ JexprKpath:i ]∧regfcom (cmds, tape, path : i : j) = regfcom (cmds, tape, path : i)[a 7→ JexprKpath:icom ];∀i, j.
regf (cmds, tape, path : i : j) = regf (cmds, tape, path : i)∧regfcom (cmds, tape, path : i : j) = regfcom (cmds, tape, path : i), иначе.Рис. 26. Функции вычисления состояния переменных regf и regfcompath00,10,1,20,1,2,3regf(cmds, tape, path)⊥⊥⊥[a 7→ 9]regfcom (cmds, tape, path)⊥⊥⊥⊥Табл. 4. Значение функций regf и regfcom для примера из табл.
390Функции значения переменных естественным образом обобщаются нафункции вычисления значения выражений e ⇀ Val. Когда значения параметровcmds, tape (и path) очевидны из контекста, мы обозначаем эти функции J−Kpath иJ−Kpathcom (или J−K и J−Kcom ).Состояние подсистемы памяти MPOP является тройкой ⟨Evt, Ord, Prop⟩, гдеEvt ⊆ ReqSet — это множество запросов в подсистеме, Ord ⊆ Evt × Evt — частичный порядок на запросах и Prop ⊆ Tid × Evt — функция, которая по идентификатору потока возвращает множество запросов, о которых он осведомлён. Запросreq является тройкой ⟨tid, path, reqinfo⟩, где tid — идентификатор потока, которыйотправил это запрос, path — путь до соответствующего экземпляра инструкции иreqinfo — информация о типе и параметрах запроса:reqinfo ::= rd ℓ | wr ℓ : val | dmb.Запрос чтения параметризован целевой локацией, запрос записи — целевой локацией и записываемым значением.Полное состояние ARM-машины StateARM — это тройка ⟨MPOP , iordf, tapef⟩,где MPOP — это состояние подсистемы памяти, iordf : Tid → List ReqSet — этофункция, которая для потока возвращает упорядоченный список отправленныхим запросов чтения и tapef : Tid → Tape представляет плёнки потоков (состояние подсистемы управления).
Компонента iordf используется для разрешения конфликтов, вызванных отправлением запросов чтения к одной локации не по порядку (подробнее описано ниже в правиле Получение ответа на чтение).Начальное состояние ARM-машины имеет инициализирующие записи вовсе локации Evtinit ≜ {⟨0tid , [], wr ℓ : 0⟩ | ℓ ∈ Loc}, где соответствующие запросыне упорядочены и о них осведомлены все потоки:sinit ≜ ⟨MPOP = ⟨Evtinit , ∅, Tid × Evtinit ⟩, iordf = λtid. [], tapef = λtid. ⊥⟩.Наша формализация ARM-машины имеет 12 правил перехода.
Эти переходы в математической нотации приведены в приложении Б, ниже приведено ихнеформальное описание.Загрузка инструкции tid path (fetch instruction) добавляет экземпляр инструкции с состоянием none в плёнку tape потока tid.Уведомление потока tid о запросе e (propagate) добавляет e во множествоMPOP .Prop(tid). Правило проверяет, что поток уведомлён о всех запросахe′ таких, что e′ <Ord e. Правило также добавляет по ребру (e, e′′ ) в Ord91для каждого запроса e′′ , который не переупорядочиваем с e и о которомосведомлён поток e.tid, но не поток tid.Выбор ветки условного перехода tid path (branch commit) выполняет экземпляр инструкции условного перехода if − goto и удаляет одну из ветокспекулятивного исполнения из плёнки потока tid вместе с соответствующими ей запросами из подсистемы памяти.Завершение барьера ld tid path (fence commit) проверяет, что предшествующие экземпляры чтения завершены (committed), и помечает экземпляр барьера как выполненный.Завершение барьера sy tid path проверяет, что все предшествующие экземпляры завершены, помечает экземпляр барьера как выполненный и отправляет запрос барьера в подсистему памяти.Подготовка записи tid path ℓ val (write pending) устанавливает состояниеэкземпляра записи в pending ℓ val, где ℓ и val являются целевой локациейи записываемым значением, которые вычисляются в коде инструкции.Завершение записи tid path ℓ val (write commit) устанавливает состояниеэкземпляра записи в com _ ℓ val.
Это правило также отправляет соответствующий запрос в подсистему памяти, но только в том случае, если вплёнке потока нет последующего экземпляра записи в ту же локацию, исполнение которого завершено. Кроме того, правило перезапускает некоторые исполнения экземпляров чтения, целевой локацией которых являетсяℓ, а также экземпляры произвольных типов, зависящие от этих экземпляров чтения.
Правило имеет несколько ограничений. Так, исполнение всехэкземпляров барьеров памяти и условных переходов, предшествующихэкземпляру (tid, path), должно быть завершено; все предшествующие экземпляры должны иметь полностью вычисленные целевые локации (fullydetermined addresses), т.е. соответствующие выражения адресов должныбыть вычисляемы к значению с помощью функции regfcom .Отправка запроса на чтение tid path ℓ (read issue) добавляет соответствующий запрос в подсистему хранения, а также в список отправленных запросов (компонента iordf(tid)). Правило требует, чтобы исполнение предшествующих экземпляров барьеров было завершено.Получение ответа на чтение tid path tid′ path′ ℓ val (read satisfy) и Игнорирование ответа на чтение tid path tid′ path′ ℓ val (read satisfy fail) получает ответ на запрос ⟨tid, path, rd ℓ⟩ из запроса записи ⟨tid′ , path′ , wr ℓ :92val⟩, если между ними нет запроса в отношении Ord.
Правила переходов удаляют запрос на чтение из подсистемы памяти. Если в плёнке потока не присутствует предшествующего экземпляра чтения из той же локации, которой отправил запрос в подсистему памяти после экземпляра(tid, path) (что определяется с помощью компоненты iordf(tid)) и получилответ от другого запроса записи, то применяется переход Получение ответа на чтение. Этот переход присваивает экземпляру чтения состояниеsat pln ⟨tid′ , path′ , wr ℓ : val⟩ и перезапускает некоторые последующиеэкземпляры чтения из той же локации вместе с зависимостями, если этотребуется для восстановления корректности.
Если условие не выполняется, то применяется переход Игнорирование ответа на чтение, которыйперезапускает экземпляр (tid, path).Получение ответа на чтение от подготовленной записи tid path path′ ℓ val(read satisfy from in-flight write) устанавливает состояние экземпляра чтения в sat inflight ⟨tid, path′ , wr ℓ : val⟩ при условии, что существуетподготовленный незавершенный экземпляр записи (tid, path′ ) и не существует экземпляра записи в ту же локацию между ними или экземплярачтения из той же локации, который получил ответ от другой записи. Это правило также, как и правило Получение ответа на чтение,перезапускает некоторые последующие экземпляры чтения.Завершение чтения tid path (read commit) проверяет, что все предшествующие экземпляры барьеров памяти и условных переходов завершены, всепредшествующие экземпляры имеют полностью определённые адреса, иприсваивает экземпляру состояние sat com _.3.5Формальное определение обещающей моделиСостояние обещающей машины StatePromise является парой ⟨T S, M ⟩.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
