Wyniki wyszukiwania

Sortuj według:

Ogranicz wyniki do:

Simple-Named Complex-Valued Nominative Data – Definition and Basic Operations

100%

Ivanov I., Nikitchenko M., Kryvolap A., Korniłowicz A.

Formalized Mathematics

2017

tom 25

nr 3

205-216

In this paper we give a formal definition of the notion of nominative data with simple names and complex values [15, 16, 19] and formal definitions of the basic operations on such data, including naming, denaming and overlapping, following the work [19]. The notion of nominative data plays an important role in the composition-nominative approach to program formalization [15, 16] which is a development of composition programming [18]. Both approaches are compared in [14]. The composition-nominative approach considers mathematical models of computer software and data on various levels of abstraction and generality and provides mathematical tools for reasoning about their properties. In particular, nominative data are mathematical models of data which are stored and processed in computer systems. The composition-nominative approach considers different types [14, 19] of nominative data, but all of them are based on the name-value relation. One powerful type of nominative data, which is suitable for representing many kinds of data commonly used in programming like lists, multidimensional arrays, trees, tables, etc. is the type of nominative data with simple (abstract) names and complex (structured) values. The set of nominative data of given type together with a number of basic operations on them like naming, denaming and overlapping [19] form an algebra which is called data algebra. In the composition-nominative approach computer programs which process data are modeled as partial functions which map nominative data from the carrier of a given data algebra (input data) to nominative data (output data). Such functions are also called binominative functions. Programs which evaluate conditions are modeled as partial predicates on nominative data (nominative predicates). Programming language constructs like sequential execution, branching, cycle, etc. which construct programs from the existing programs are modeled as operations which take binominative functions and predicates and produce binominative functions. Such operations are called compositions. A set of binominative functions and a set of predicates together with appropriate compositions form an algebra which is called program algebra. This algebra serves as a semantic model of a programming language. For functions over nominative data a special computability called abstract computability is introduces and complete classes of computable functions are specified [16]. For reasoning about properties of programs modeled as binominative functions a Floyd-Hoare style logic [1, 2] is introduced and applied [12, 13, 8, 11, 9, 10]. One advantage of this approach to reasoning about programs is that it naturally handles programs which process complex data structures (which can be quite straightforwardly represented as nominative data). Also, unlike classical Floyd-Hoare logic, the mentioned logic allows reasoning about assertions which include partial pre- and post-conditions [11]. Besides modeling data processed by programs, nominative data can be also applied to modeling data processed by signal processing systems in the context of the mathematical systems theory [4, 6, 7, 5, 3].

Event-Based Proof of the Mutual Exclusion Property of Peterson’s Algorithm

100%

Ivanov I., Nikitchenko M., Abraham U.

Formalized Mathematics

2015

tom 23

nr 4

325-331

Proving properties of distributed algorithms is still a highly challenging problem and various approaches that have been proposed to tackle it [1] can be roughly divided into state-based and event-based proofs. Informally speaking, state-based approaches define the behavior of a distributed algorithm as a set of sequences of memory states during its executions, while event-based approaches treat the behaviors by means of events which are produced by the executions of an algorithm. Of course, combined approaches are also possible. Analysis of the literature [1], [7], [12], [9], [13], [14], [15] shows that state-based approaches are more widely used than event-based approaches for proving properties of algorithms, and the difficulties in the event-based approach are often emphasized. We believe, however, that there is a certain naturalness and intuitive content in event-based proofs of correctness of distributed algorithms that makes this approach worthwhile. Besides, state-based proofs of correctness of distributed algorithms are usually applicable only to discrete-time models of distributed systems and cannot be easily adapted to the continuous time case which is important in the domain of cyber-physical systems. On the other hand, event-based proofs can be readily applied to continuous-time / hybrid models of distributed systems. In the paper [2] we presented a compositional approach to reasoning about behavior of distributed systems in terms of events. Compositionality here means (informally) that semantics and properties of a program is determined by semantics of processes and process communication mechanisms. We demonstrated the proposed approach on a proof of the mutual exclusion property of the Peterson’s algorithm [11]. We have also demonstrated an application of this approach for proving the mutual exclusion property in the setting of continuous-time models of cyber-physical systems in [8]. Using Mizar [3], in this paper we give a formal proof of the mutual exclusion property of the Peterson’s algorithm in Mizar on the basis of the event-based approach proposed in [2]. Firstly, we define an event-based model of a shared-memory distributed system as a multi-sorted algebraic structure in which sorts are events, processes, locations (i.e. addresses in the shared memory), traces (of the system). The operations of this structure include a binary precedence relation ⩽ on the set of events which turns it into a linear preorder (events are considered simultaneous, if e1 ⩽ e2 and e2 ⩽ e1), special predicates which check if an event occurs in a given process or trace, predicates which check if an event causes the system to read from or write to a given memory location, and a special partial function “val of” on events which gives the value associated with a memory read or write event (i.e. a value which is written or is read in this event) [2]. Then we define several natural consistency requirements (axioms) for this structure which must hold in every distributed system, e.g. each event occurs in some process, etc. (details are given in [2]). After this we formulate and prove the main theorem about the mutual exclusion property of the Peterson’s algorithm in an arbitrary consistent algebraic structure of events. Informally, the main theorem states that if a system consists of two processes, and in some trace there occur two events e1 and e2 in different processes and each of these events is preceded by a series of three special events (in the same process) guaranteed by execution of the Peterson’s algorithm (setting the flag of the current process, writing the identifier of the opposite process to the “turn” shared variable, and reading zero from the flag of the opposite process or reading the identifier of the current process from the “turn” variable), and moreover, if neither process writes to the flag of the opposite process or writes its own identifier to the “turn” variable, then either the events e1 and e2 coincide, or they are not simultaneous (mutual exclusion property).

Ograniczanie wyników

2 Formalized Mathematics

2 Ivanov I.

2 Nikitchenko M.

1 Abraham U.

1 Korniłowicz A.

1 Kryvolap A.

1 2017

1 2015

Wyniki wyszukiwania

Simple-Named Complex-Valued Nominative Data – Definition and Basic Operations

Event-Based Proof of the Mutual Exclusion Property of Peterson’s Algorithm