Что такое индуктивный инвариант простой параллельной программы?

Question

Что такое индуктивный инвариант простой параллельной программы?

Вот простая параллельная программа из статьи Лесли Лампорта " Обучение параллелизму ".

Рассмотрим $N$ процессы, пронумерованные от 0 до $N-1$, в которых каждый процесс $ i $ выполняется

x[i] := 1
y[i] := x[(i - 1) % N]

и останавливается, где каждый x[i] изначально равен 0. (Чтение и запись каждого x[i] считаются атомными.)

Этот алгоритм удовлетворяет следующему свойству: после того, как каждый процесс остановлен, y[i] равно 1 для хотя бы одного процесса $i$. Это легко проверить: последний процесс $ i $ для записи y[i] должен установить его на 1.

Затем Лампорт отмечает, что

Но этот процесс не устанавливает y[i] к 1, потому что это был последний процесс, чтобы написать $ y $.
Алгоритм удовлетворяет этому свойству, поскольку поддерживает индуктивный инвариант. Вы знаете, что это за инвариант? Если нет, то вы не совсем понимаете, почему алгоритм удовлетворяет этому свойству.

Следовательно,

Что такое индуктивный инвариант параллельной программы?

4

concurrency invariants correctness tla+ tlaps

Источник

user1833118 28 июл '14 в 06:44

2 ответа

Решение

TL;DR

Индуктивный инвариант этой программы в синтаксисе TLA+:

/\ \A i \in 0..N-1 : (pc[i] \in {"s2", "Done"} => x[i] = 1) 
/\ (\A i \in 0..N-1 : pc[i] = "Done") => \E i \in 0..N-1 : y[i] = 1

Что такое индуктивный инвариант?

Индуктивный инвариант - это инвариант, который удовлетворяет следующим двум условиям:

Init => Inv
Inv /\ Next => Inv'

где:

Inv является индуктивным инвариантом
Init это предикат, который описывает начальное состояние
Next это предикат, который описывает переходы между состояниями.

Зачем использовать индуктивные инварианты?

Обратите внимание, что индуктивный инвариант касается только текущего состояния и следующего состояния. В нем нет ссылок на историю выполнения, речь идет не о прошлом поведении системы.

В разделе 7.2.1 Принципов и спецификаций параллельных систем (общеизвестных как Гипербука TLA+) Лэмпорт описывает, почему он предпочитает использовать индуктивные инварианты, а не поведенческие доказательства (т. Е. Те, которые ссылаются на историю выполнения).

Поведенческие доказательства можно сделать более формальными, но я не знаю никакого практического способа сделать их полностью формальными, то есть написать исполняемые описания реальных алгоритмов и формальные поведенческие доказательства того, что они удовлетворяют свойствам корректности. Это одна из причин, почему за более чем 35 лет написания параллельных алгоритмов я обнаружил, что поведенческие рассуждения ненадежны для более сложных алгоритмов. Я полагаю, что еще одной причиной является то, что поведенческие доказательства по своей природе являются более сложными, чем основанные на состоянии, доказательства для достаточно сложных алгоритмов. Это заставляет людей писать менее строгие поведенческие доказательства для этих алгоритмов, особенно без каких-либо формальных доказательств, которые могли бы служить ориентиром.
Чтобы избежать ошибок, мы должны думать с точки зрения состояний, а не с точки зрения казни... Тем не менее, поведенческие рассуждения предоставляют другой способ мышления об алгоритме, и мышление всегда полезно. Поведенческие рассуждения плохи, только если они используются вместо основанных на состоянии рассуждений, а не в дополнение к ним.

Некоторые предварительные

Свойство, которое мы заинтересованы в доказательстве (в синтаксисе TLA+):

(\A i \in 0..N-1 : pc[i] = "Done") => \E i \in 0..N-1 : y[i] = 1

Здесь я использую соглашение PlusCal, описывающее состояние управления каждым процессом с помощью переменной с именем "pc" (я думаю, что это "счетчик программ").

Это свойство является инвариантом, но это не индуктивный инвариант, поскольку он не удовлетворяет указанным выше условиям.

Вы можете использовать индуктивный инвариант для доказательства свойства, написав доказательство, которое выглядит следующим образом:

1. Init => Inv
2. Inv /\ Next => Inv'
3. Inv => DesiredProperty

Чтобы придумать индуктивный инвариант, нам нужно присвоить метки каждому шагу алгоритма, назовем их "s1", "s2" и "Done", где "Done" - состояние терминала для каждого процесса.

s1: x[self] := 1;
s2: y[self] := x[(self-1) % N]

Придумывая индуктивный инвариант

Рассмотрим состояние программы, когда она находится в предпоследнем (предпоследнем) состоянии выполнения.

В последнем состоянии выполнения, pc[i]="Done" для всех значений я. В предпоследнем состоянии, pc[i]="Done" для всех значений i, кроме одного, назовем его j, где pc[j]="s2",

Если процесс находится в состоянии "Готово", то должно быть верно, что x[i]=1, поскольку процесс должен выполнить инструкцию "s1". Точно так же процесс j, который находится в состоянии "s2", должен также выполнить инструкцию "s1", поэтому должно быть верно, что x[j]=1,

Мы можем выразить это как инвариант, который оказывается индуктивным инвариантом.

\A i \in 0..N-1 : (pc[i] \in {"s2", "Done"} => x[i] = 1)

Модель PlusCal

Чтобы доказать, что наш инвариант является индуктивным инвариантом, нам нужна правильная модель, которая имеет Init предикат состояния и Next предикат состояния.

Мы можем начать с описания алгоритма в PlusCal. Это очень простой алгоритм, поэтому я назову его "Простой".

--algorithm Simple

variables
    x = [i \in 0..N-1 |->0];
    y = [i \in 0..N-1 |->0];

process Proc \in 0..N-1 
begin
    s1: x[self] := 1;
    s2: y[self] := x[(self-1) % N]
end process

end algorithm

Перевод на TLA+

Мы можем перевести модель PlusCal в TLA+. Вот как это выглядит, когда мы переводим PlusCal в TLA+ (я пропустил условие завершения, потому что оно нам здесь не нужно).

------------------------------- MODULE Simple -------------------------------

EXTENDS Naturals

CONSTANTS N

VARIABLES x, y, pc

vars == << x, y, pc >>

ProcSet == (0..N-1)

Init == (* Global variables *)
        /\ x = [i \in 0..N-1 |->0]
        /\ y = [i \in 0..N-1 |->0]
        /\ pc = [self \in ProcSet |-> "s1"]

s1(self) == /\ pc[self] = "s1"
            /\ x' = [x EXCEPT ![self] = 1]
            /\ pc' = [pc EXCEPT ![self] = "s2"]
            /\ y' = y

s2(self) == /\ pc[self] = "s2"
            /\ y' = [y EXCEPT ![self] = x[(self-1) % N]]
            /\ pc' = [pc EXCEPT ![self] = "Done"]
            /\ x' = x

Proc(self) == s1(self) \/ s2(self)

Next == (\E self \in 0..N-1: Proc(self))
           \/ (* Disjunct to prevent deadlock on termination *)
              ((\A self \in ProcSet: pc[self] = "Done") /\ UNCHANGED vars)

Spec == Init /\ [][Next]_vars
=============================================================================

Обратите внимание, как это определяет Init а также Next предикаты состояния.

Индуктивный инвариант в TLA+

Теперь мы можем указать индуктивный инвариант, который мы хотим доказать. Мы также хотим, чтобы наш индуктивный инвариант подразумевал свойство, которое мы заинтересованы в доказательстве, поэтому мы добавляем его как конъюнкцию.

Inv == /\ \A i \in 0..N-1 : (pc[i] \in {"s2", "Done"} => x[i] = 1)
       /\ (\A i \in 0..N-1 : pc[i] = "Done") => \E i \in 0..N-1 : y[i] = 1

Неофициальные рукопожатия "доказательство"

1. `Init => Inv`

Должно быть очевидно, почему это так, поскольку предшествующие Inv все ложно, если Init правда.

2. `Inv /\ Next => Inv'`

Первый союз Инв

(\A i \in 0..N-1 : (pc[i] \in {"s2", "Done"} => x[i] = 1))'

Интересный случай, когда pc[i]="s1" а также pc'[i]="s2" для некоторых я. По определению s1 Должно быть понятно, почему это так.

Второй союз Инв

((\A i \in 0..N-1 : pc[i] = "Done") => \E i \in 0..N-1 : y[i] = 1)'

Интересный случай - тот, который мы обсуждали ранее, где pc[i]="Done" для всех значений i, кроме одного, j, где pc[j]="s2",

По первому соединению Inv мы знаем, что x[i]=1 для всех значений я.

От s2, y'[j]=1,

3. `Inv => DesiredProperty`

Здесь наше желаемое свойство

(\A i \in 0..N-1 : pc[i] = "Done") => \E i \in 0..N-1 : y[i] = 1

Обратите внимание, что мы только что добавили интересующее нас свойство к инварианту, так что это тривиально доказать.

Формальное доказательство с TLAPS

Вы можете использовать TLA+ Proof System (TLAPS), чтобы написать формальное доказательство, которое можно механически проверить, чтобы определить, верно ли оно.

Вот доказательство, которое я написал и проверил, используя TLAPS, который использует индуктивный инвариант для доказательства желаемого свойства. (Примечание: это первое доказательство, которое я когда-либо написал с использованием TLAPS, так что имейте в виду, что это было написано новичком).

AtLeastOneYWhenDone == (\A i \in 0..N-1 : pc[i] = "Done") => \E i \in 0..N-1 : y[i] = 1

TypeOK == /\ x \in [0..N-1 -> {0,1}]
          /\ y \in [0..N-1 -> {0,1}]
          /\ pc \in [ProcSet -> {"s1", "s2", "Done"}]

Inv == /\ TypeOK
       /\ \A i \in 0..N-1 : (pc[i] \in {"s2", "Done"} => x[i] = 1)
       /\ AtLeastOneYWhenDone

ASSUME NIsInNat == N \in Nat \ {0}       

\* TLAPS doesn't know this property of modulus operator
AXIOM ModInRange == \A i \in 0..N-1: (i-1) % N \in 0..N-1


THEOREM Spec=>[]AtLeastOneYWhenDone
<1> USE DEF ProcSet, Inv
<1>1. Init => Inv
    BY NIsInNat DEF Init, Inv, TypeOK, AtLeastOneYWhenDone
<1>2. Inv /\ [Next]_vars => Inv'
  <2> SUFFICES ASSUME Inv,
                      [Next]_vars
               PROVE  Inv'
    OBVIOUS
  <2>1. CASE Next
    <3>1. CASE \E self \in 0..N-1: Proc(self)
      <4> SUFFICES ASSUME NEW self \in 0..N-1,
                          Proc(self)
                   PROVE  Inv'
        BY <3>1 
      <4>1. CASE s1(self)
        BY <4>1, NIsInNat DEF s1, TypeOK, AtLeastOneYWhenDone
      <4>2. CASE s2(self)
        BY <4>2, NIsInNat, ModInRange DEF s2, TypeOK, AtLeastOneYWhenDone
      <4>3. QED
        BY <3>1, <4>1, <4>2 DEF Proc
    <3>2. CASE (\A self \in ProcSet: pc[self] = "Done") /\ UNCHANGED vars
        BY <3>2 DEF TypeOK, vars, AtLeastOneYWhenDone
    <3>3. QED
      BY <2>1, <3>1, <3>2 DEF Next
  <2>2. CASE UNCHANGED vars
    BY <2>2 DEF TypeOK, vars, AtLeastOneYWhenDone
  <2>3. QED
    BY <2>1, <2>2
<1>3. Inv => AtLeastOneYWhenDone
    OBVIOUS
<1>4. QED
    BY <1>1, <1>2, <1>3, PTL DEF Spec

Обратите внимание, что в доказательстве, использующем TLAPS, вы должны иметь инвариант проверки типа (он называется TypeOK выше), и вам также нужно обрабатывать "состояния заикания", когда ни одна из переменных не изменяется, поэтому мы используем [Next]_vars вместо Next,

Вот суть с полной моделью и доказательством.

5

Источник

user742 08 сен '17 в 03:49

Другие вопросы по тегам concurrency invariants correctness tla+ tlaps

user577603 29 июл '14 в 16:20 2014-07-29 16:20 · Accepted Answer · 2014-07-29 16:20

x s моделирует следующее поведение: x[i] является 1 если и только если процесс i уже побежал. Естественно, после того, как все процессы завершены, все x S, таким образом, установлены на 1,

y немного сложнее: y[i] устанавливается, если x[i-1] был установлен, то есть y[i] является 1 если и только если предшественник i уже бежал, когда i делал свое письмо y,

Инвариант программы: если процесс установлен y[i] , должно быть уже установлено x[i] в 1, Это верно независимо от того, y[i] установлен в 0 или же 1,

Доказать этот инвариант довольно легко: в начале, ни один из y s установлен, поэтому он выполняется тривиально. Во время выполнения программы каждая запись в y[i] последовательность после записи в x[i], Поэтому инвариант также выполняется для каждого шага программы впоследствии.

Дальнейшие рассуждения звучат так: последний процесс заканчивает наборы y[i] в 1 потому что, по определению, являющегося последним процессом, его предшественник уже должен был завершить выполнение в этой точке (т.е. его y значение уже установлено). Что означает, из-за инварианта, его x значение (которое определяет последний процесс " y значение) должно быть 1,

Другой способ взглянуть на это: вы не можете найти порядок выполнения, в котором все y s установлены в 0, Это потребует выполнения всех процессов раньше, чем их предшественник. Однако, поскольку наши процессы расположены в кольце (то есть, если я буду следовать цепочке предшественников, я в конечном итоге снова окажусь в моей начальной точке), это приводит к противоречию, что по крайней мере один процесс должен завершиться, прежде чем он записал в y,