Главная » Просмотр файлов » 3. Verification of sequential and concurrent programs. Apt_ Olderog (3rd edition) (2010)

3. Verification of sequential and concurrent programs. Apt_ Olderog (3rd edition) (2010) (811405), страница 78

Файл №811405 3. Verification of sequential and concurrent programs. Apt_ Olderog (3rd edition) (2010) (3. Verification of sequential and concurrent programs. Apt_ Olderog (3rd edition) (2010).pdf) 78 страница3. Verification of sequential and concurrent programs. Apt_ Olderog (3rd edition) (2010) (811405) страница 782020-08-25СтудИзба
Просмтор этого файла доступен только зарегистрированным пользователям. Но у нас супер быстрая регистрация: достаточно только электронной почты!

Текст из файла (страница 78)

The correctness of this program depends on the fairness assumption.For pedagogical reasons we first study an example where the main idea forthe termination argument is exercised.Example 12.7. Consider a programS ≡ do B1 → S1 ⊓⊔. . .⊓⊔Bn → Sn odwith the following property: the index set {1, . . . , n} is partitioned into setsK and L with L 6= ∅, such that executing any subprogram Sk with k ∈ Kdoes not change the program state, whereas executing any subprogram Sℓwith ℓ ∈ L yields a new program state which is closer to a terminal state ofS.More specifically, we takeB ≡ x 6= 0, Sk ≡ skip for k ∈ K and Sℓ ≡ x := x − 1 for ℓ ∈ L,where x is an integer variable.

For any choice of K and L we wish to prove|=fair {x ≥ 0} S {x = 0}with the help of the fair repetition rule 39′ of system FN. As invariant wetakep ≡ x ≥ 0.This choice obviously satisfies premise (1) of rule 39′ .To find an appropriate bound function, let us first consider the case whereK = {1, .

. ., n − 1} and L = {n}; that is, whereS ≡ do x 6= 0 → skip ⊓⊔. . .⊓⊔ x 6= 0 → skip ⊓⊔ x 6= 0 → x := x − 1 od.|{z}n − 1 timesAs in Example 12.6, we observe a hierarchy of changes:• executing one of the n − 1 subprograms skip; the assumption of fairnessimplies that the subprogram Sn ≡ x := x − 1 cannot be neglected forever,• executing Sn decrements x, thus bringing us closer to the termination ofS.12.9 Case Study: Asynchronous Fixed Point Computation447Since the number of rounds through the loop during which Sn is neglectedis counted by the scheduling variable zn referring to Sn , we arrive at thebound functiont ≡ (x, zn )ranging over the well-founded structure W = N × N ordered lexicographicallyby <lex .Clearly, p and t satisfy premise (3) of rule 39′ .

By the simple form of thesubprograms of S, checking premise (2) of rule 39′ boils down to checkingthe following implications:• for Sk ≡ skip where k ∈ {1, . . ., n − 1}:x > 0 ∧ zn ≥ 0 ∧ (x, zn + 1) = α → (x, zn ) <lex α,• for Sn ≡ x := x − 1:x > 0 ∧ zn ≥ 0 ∧ ∃zn ≥ 0 : (x, zn ) = α → (x − 1, zn ) <lex α.These implications are obviously true.Thus the fair repetition rule 39′ and the rule of consequence yield|=fair {x ≥ 0} S {x = 0}as claimed.Let us now turn to the general case of sets K and L where it is not onlysubprogram Sn that is responsible for decrementing x, but any subprogramSℓ with ℓ ∈ L will do. Then the number of rounds neglecting any of these subprograms is given by min {zℓ | ℓ ∈ L} with zℓ being the scheduling variablereferring to Sℓ .

This leads tot ≡ (x, min {zℓ | ℓ ∈ L})as a suitable bound function for the general case.⊓⊔Before we formulate the problem we wish to solve, we need to introducesome auxiliary notions first. A partial order is a pair (A, ⊑ ) consisting of aset A and a reflexive, antisymmetric and transitive relation ⊑ on A.Consider now a partial order (A, ⊑ ). Let a ∈ A and X ⊑ A. Then a iscalled the least element of X if a ∈ X and a ⊑ x for all x ∈ X. The element ais called an upper bound of X if x ⊑ a for all x ∈ X. Note that upper boundsof X need not be elements of X. Let U be the set of all upper bounds of X.Then a is called the least upper bound of X if a is the least element of U .A partial order (A, ⊑ ) is called complete if A contains a least elementand if for every ascending chaina0 ⊑ a1 ⊑ a2 .

. .44812 Fairnessof elements from A the set{a0 , a1 , a2 , . . .}has a least upper bound.Now we turn to the problem of computing fixed points. Let (L, ⊑ ) be acomplete partial order. For x, y ∈ L we write x ⊏ y if x ⊑ y and x 6= y. Let⊐ denote the inverse of ⊏ ; so x ⊐ y if y ⊏ x holds. Assume that (L, ⊑ )has the finite chain property, that is, every ascending chainx1 ⊑ x2 ⊑ x3 ⊑ .

. .of elements xi ∈ L stabilizes. In other words, there is no infinite increasingchainx1 ⊏ x2 ⊏ x3 ⊏ . . .in L, or equivalently, the inverse relation ⊐ is well-founded on L.We consider here the n-fold Cartesian product Ln of L for some n ≥ 2.The relation ⊑ is extended componentwise from L to Ln :(x1 , . . ., xn ) ⊑ (y1 , . . ., yn ) iff ∀(1 ≤ i ≤ n) : xi ⊑ yi .We also extend the relation ⊏ and its inverse ⊐ :(x1 , . .

., xn ) ⊏ (y1 , . . ., yn ) iff (x1 , . . ., xn ) ⊑ (y1 , . . ., yn )and (x1 , . . ., xn ) 6= (y1 , . . ., yn ),(x1 , . . ., xn ) ⊐ (y1 , . . ., yn ) iff(y1 , . . ., yn ) ⊏ (x1 , . . ., xn ).Then also the pair (Ln , ⊑ ) is a complete partial order with the finite chainproperty. Let ∅ denote the least element in Ln .Consider now a functionF : Ln → Lnwhich is monotonic under ⊑ ; that is, whenever (x1 , . .

., xn ) ⊑ (y1 , . . ., yn )then F (x1 , . . ., xn ) ⊑ F (y1 , . . ., yn ).By Fi we denote the ith component functionFi : Ln → Lof F . Thus we define Fi as follows:Fi (x1 , . . ., xn ) = yi iff F (x1 , . . ., xn ) = (y1 , . . ., yn ).Since ⊑ is defined componentwise and F is monotonic, the functions Fi arealso monotonic under ⊑ .By a general theorem due to Knaster and Tarski (see Tarski [1955]), F hasa least fixed point µF ∈ Ln ; that is,F (µF ) = µF12.9 Case Study: Asynchronous Fixed Point Computation449andF (x1 , . .

., xn ) = (x1 , . . ., xn ) implies µF ⊑ (x1 , . . ., xn ).Usually µF is computed as follows. Starting with the least element ∅ in Lnthe operator F is applied iteratively:∅ ⊑ F (∅) ⊑ F (F (∅)) ⊑ F (F (F (∅))) ⊑ . . . .By the finite chain property of Ln , this iteration process will surely stabilizeby the least fixed point µF . Since an application of F requires a simultaneousupdate of all n components of its arguments, this method of computing µFis called a synchronous fixed point computation.Following Cousot and Cousot [1977b] we are interested here in a moreflexible method. We wish to compute µF asynchronously by employing nsubprograms Si , for i ∈ {1, . .

. , n}, where each of them is allowed to apply only the ith component function Fi . These subprograms are activatednondeterministically by the following program:AFIX ≡ do B → x1 := F1 (x̄)⊓⊔. . .⊓⊔B → xn := Fn (x̄) od,where x̄ ≡ (x1 , . . ., xn ) and B ≡ x̄ 6= F (x̄). In general AFIX will not computeµF , but the claim is that it will do so under the assumption of fairness:|=fair {x̄ = ∅} AFIX {x̄ = µF }.(12.29)This correctness result is a special case of a more general theorem proved inCousot and Cousot [1977b].We would like to prove (12.29) in the system FN. To this end, we proceedin two steps.Step 1 We start with an informal analysis of AFIX. Consider a computationξ :< AFIX, σ >=< S1 , σ 1 > → . . . → < Sj , σ j > → . .

.of AFIX and the abbreviations σ j (x̄) = (σ j (x1 ), . . ., σ j (xn )) for j ≥ 1 andFi [x̄] = (x1 , . . ., xi−1 , Fi (x̄), xi+1 , . . ., xn )for i ∈ {1, . . . , n}. Since σ 1 (x̄) = ∅ holds and the component functions Fi aremonotonic, the assertion∅ ⊑ x̄ ⊑ Fi [x̄] ⊑ µF(12.30)is true for i ∈ {1, . . . , n} in every state σ j of ξ. Thus, by the least fixed pointproperty, x̄ = µF holds as soon as AFIX has terminated with x̄ = F (x̄).But why does AFIX terminate? Note that by (12.30) AFIX produces anascending chainσ 1 (x̄) ⊑ . . .

⊑ σ j (x̄) ⊑ . . .45012 Fairnessof values in the variable x̄. That there exists a state σ j in which x̄ = F (x̄)relies on the following two facts.(i) By the finite chain property of L and hence Ln , the values σ j (x̄) ∈ Lncannot be increased infinitely often.(ii) By the assumption of fairness, the values σ j (x̄) cannot be constantarbitrarily long without increasing.(i) is clear, but (ii) needs a proof. Consider some nonterminal state σ jin ξ (thus satisfying B ≡ x̄ 6= F (x̄)) for which either σ j (x̄) = σ 1 (x̄) (start)or σ j−1 (x̄) ⊏ σ j (x̄) (increase just happened) holds. Then we can find twoindex sets K and L, both depending on σ j , which partition the subprogramsS1 , .

. ., Sn of AFIX into subsets {Sk | k ∈ K} and {Sℓ | ℓ ∈ L} such that theSk stabilize the values of x̄, so for k ∈ K, x̄ = Fk [x̄] holds in σ j , whereas theSℓ increase the values of x̄, so for ℓ ∈ L, x̄ ⊏ Fℓ [x̄] holds in σ j . Note thatL 6= ∅ holds because σ j is nonterminal.Thus, as long as subprograms Sk with k ∈ K are executed, the programAFIX generates states σ j+1 , σ j+2 , .

. . satisfyingσ j (x̄) = σ j+1 (x̄) = σ j+2 (x̄) = . . . .But as soon as a subprogram Sℓ with ℓ ∈ L is executed in some state σ mwith j ≤ m, we get the desired next increaseσ m (x̄) ⊏ σ m+1 (x̄)after σ j . Fairness guarantees that such an increase will indeed happen.The situation is close to that investigated in Example 12.7, except for thefollowing changes:• instead of decrementing an integer variable x, here x̄ = (x1 , . .

., xn ) isincreased in the ordering ⊏ on Ln ,• the number of possible increases of x̄ is unknown but finite,• the index sets K and L depend on the state σ j .Step 2 With this informal discussion in mind, we are now prepared for theformal correctness proof. The essential step is the application of the fairrepetition rule 39′ . A suitable invariant isp≡n^(∅ ⊑ x̄ ⊑ Fi [x̄] ⊑ µF ).i=1Clearly, p satisfies premise (1′ ) of rule 39′ .By analogy to Example 12.7, we take as the well-founded structure the setW = Ln × Nordered lexicographically as follows:12.9 Case Study: Asynchronous Fixed Point Computation451(x̄, u) <lex (ȳ, v) iff x̄ ⊐ ȳ or (x̄ = ȳ and u < v),with the inverse relation ⊐ in the first component because increasing x̄means getting closer to the desired fixed point, hence termination.

Характеристики

Список файлов книги

Свежие статьи
Популярно сейчас
Почему делать на заказ в разы дороже, чем купить готовую учебную работу на СтудИзбе? Наши учебные работы продаются каждый год, тогда как большинство заказов выполняются с нуля. Найдите подходящий учебный материал на СтудИзбе!
Ответы на популярные вопросы
Да! Наши авторы собирают и выкладывают те работы, которые сдаются в Вашем учебном заведении ежегодно и уже проверены преподавателями.
Да! У нас любой человек может выложить любую учебную работу и зарабатывать на её продажах! Но каждый учебный материал публикуется только после тщательной проверки администрацией.
Вернём деньги! А если быть более точными, то автору даётся немного времени на исправление, а если не исправит или выйдет время, то вернём деньги в полном объёме!
Да! На равне с готовыми студенческими работами у нас продаются услуги. Цены на услуги видны сразу, то есть Вам нужно только указать параметры и сразу можно оплачивать.
Отзывы студентов
Ставлю 10/10
Все нравится, очень удобный сайт, помогает в учебе. Кроме этого, можно заработать самому, выставляя готовые учебные материалы на продажу здесь. Рейтинги и отзывы на преподавателей очень помогают сориентироваться в начале нового семестра. Спасибо за такую функцию. Ставлю максимальную оценку.
Лучшая платформа для успешной сдачи сессии
Познакомился со СтудИзбой благодаря своему другу, очень нравится интерфейс, количество доступных файлов, цена, в общем, все прекрасно. Даже сам продаю какие-то свои работы.
Студизба ван лав ❤
Очень офигенный сайт для студентов. Много полезных учебных материалов. Пользуюсь студизбой с октября 2021 года. Серьёзных нареканий нет. Хотелось бы, что бы ввели подписочную модель и сделали материалы дешевле 300 рублей в рамках подписки бесплатными.
Отличный сайт
Лично меня всё устраивает - и покупка, и продажа; и цены, и возможность предпросмотра куска файла, и обилие бесплатных файлов (в подборках по авторам, читай, ВУЗам и факультетам). Есть определённые баги, но всё решаемо, да и администраторы реагируют в течение суток.
Маленький отзыв о большом помощнике!
Студизба спасает в те моменты, когда сроки горят, а работ накопилось достаточно. Довольно удобный сайт с простой навигацией и огромным количеством материалов.
Студ. Изба как крупнейший сборник работ для студентов
Тут дофига бывает всего полезного. Печально, что бывают предметы по которым даже одного бесплатного решения нет, но это скорее вопрос к студентам. В остальном всё здорово.
Спасательный островок
Если уже не успеваешь разобраться или застрял на каком-то задание поможет тебе быстро и недорого решить твою проблему.
Всё и так отлично
Всё очень удобно. Особенно круто, что есть система бонусов и можно выводить остатки денег. Очень много качественных бесплатных файлов.
Отзыв о системе "Студизба"
Отличная платформа для распространения работ, востребованных студентами. Хорошо налаженная и качественная работа сайта, огромная база заданий и аудитория.
Отличный помощник
Отличный сайт с кучей полезных файлов, позволяющий найти много методичек / учебников / отзывов о вузах и преподователях.
Отлично помогает студентам в любой момент для решения трудных и незамедлительных задач
Хотелось бы больше конкретной информации о преподавателях. А так в принципе хороший сайт, всегда им пользуюсь и ни разу не было желания прекратить. Хороший сайт для помощи студентам, удобный и приятный интерфейс. Из недостатков можно выделить только отсутствия небольшого количества файлов.
Спасибо за шикарный сайт
Великолепный сайт на котором студент за не большие деньги может найти помощь с дз, проектами курсовыми, лабораторными, а также узнать отзывы на преподавателей и бесплатно скачать пособия.
Популярные преподаватели
Добавляйте материалы
и зарабатывайте!
Продажи идут автоматически
6518
Авторов
на СтудИзбе
302
Средний доход
с одного платного файла
Обучение Подробнее