Pełnotekstowe zasoby PLDML oraz innych baz dziedzinowych są już dostępne w nowej Bibliotece Nauki.
Zapraszamy na https://bibliotekanauki.pl
Preferencje help
Widoczny [Schowaj] Abstrakt
Liczba wyników

Znaleziono wyników: 4

Liczba wyników na stronie
first rewind previous Strona / 1 next fast forward last

Wyniki wyszukiwania

Wyszukiwano:
w słowach kluczowych:  parallel computing
help Sortuj według:

help Ogranicz wyniki do:
first rewind previous Strona / 1 next fast forward last
1
100%
EN
Systems of consistent linear equations with symmetric positive semidefinite matrices arise naturally while solving many scientific and engineering problems. In case of a "floating" static structure, the boundary conditions are not sufficient to prevent its rigid body motions. Traditional solvers based on Cholesky decomposition can be adapted to these systems by recognition of zero rows or columns and also by setting up a well conditioned regular submatrix of the problem that is used for implementation of a generalised inverse. Conditioning such a submatrix seems to be related with detection of so called fixing nodes such that the related boundary conditions make the structure as stiff as possible. We can consider the matrix of the problem as an unweighted non-oriented graph. Now we search for nodes that stabilize the solution well-fixing nodes (such nodes are sufficiently far away from each other and are not placed near any straight line). The set of such nodes corresponds to one type of graph center.
2
Content available remote

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

88%
EN
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).
EN
The paper deals with the problem of optimal path planning for a sensor network with mutliple mobile nodes, whose measurements are supposed to be primarily used to estimate unknown parameters of a system modelled by a partial differential equation. The adopted framework permits to consider two- or three-dimensional spatial domains and correlated observations. Since the aim is to maximize the accuracy of the estimates, a general functional defined on the relevant Fisher information matrix is used as the design criterion. Central to the approach is the parameterization of the sensor trajectories based on cubic B-splines. The resulting finite-dimensional global optimization problem is then solved using a parallel version of the tunneling algorithm. A numerical example is included to clearly demonstrate the idea presented in the paper.
4
75%
EN
This work analyses the performance of Hadoop, an implementation of the MapReduce programming model for distributed parallel computing, executing on a virtualisation environment comprised of 1 + 16 nodes running the VMWare workstation software. A set of experiments using the standard Hadoop benchmarks has been designed in order to determine whether or not significant reductions in the execution time of computations are experienced when using Hadoop on this virtualisation platform on a departmental cloud. Our findings indicate that a significant decrease in computing times is observed under these conditions. They also highlight how overheads and virtualisation in a distributed environment hinder the possibility of achieving the maximum (peak) performance.
first rewind previous Strona / 1 next fast forward last
JavaScript jest wyłączony w Twojej przeglądarce internetowej. Włącz go, a następnie odśwież stronę, aby móc w pełni z niej korzystać.