text:
Protocol for Byzantine Fault Tolerant Clock. Synchronization. Reprint from J. Vytopil, editor: Formal Techniques in Real-Time and Fault-
- Harvey Hampton
- 2 years ago
- Views:
1 Mechanical Verication of a Generalized Protocol for Byzantine Fault Tolerant Clock Synchronization Reprint from J. Vytopil, editor: Formal Techniques in Real-Time and Fault- Tolerant Systems, Nijmegen, The Netherlands, January 1992, pages 217{236; Volume 571 of Springer Verlag Lecture Notes in Computer Science. Natarajan Shankar Computer Science Laboratory SRI International Menlo Park, CA USA Abstract Schneider [Sch87] generalizes a number of protocols for Byzantine faulttolerant clock synchronization and presents a uniform proof for their correctness. We present a mechanical verication of Schneider's protocol leading to several signicant clarications and revisions. The verication was carried out with the Ehdm system [RvHO91] developed at the SRI Computer Science Laboratory. The mechanically checked proofs include the verication that the egocentric mean function used in Lamport and Melliar-Smith's Interactive Convergence Algorithm [LMS85] satises the requirements of Schneider's protocol. Our mechanical verication raises a number of issues regarding the verication of fault-tolerant, distributed, real-time protocols that are germane to the design of a special-purpose logic for such problems. This work was supported by NASA Contract NAS John Rushby, Friedrich von Henke, Fred Schneider, and Rick Butler provided considerable guidance and encouragement. I also thank Paul Miner (NASA Langley Research Center) and the referees for their comments and clarications. 1
2 1 Introduction Synchronizing clocks in the presence of faults is a classic problem in distributed computing. Even the most accurate clocks do drift at signicant rates, both with respect to a time standard and relative to each other. In order for independent processors to exhibit cooperative behavior, it is often required that their local clocks be synchronized. Such synchrony is the basis for distributed algorithms that use timeouts, time stamps, and rounds of message passing. Synchronization is also assumed when the same computation is executed on multiple, independent processors in order to mask processor failures. Synchronizing clocks in the presence of faults is a dicult problem. Maintaining synchrony by periodically broadcasting a global clock has the drawback of creating a single point of failure. The basic waytoachieve fault-tolerant synchronization is for each processor to periodically execute a protocol that involves exchanging clock values with the other processors, computing a consensus reading from these values, and appropriately adjusting its local clock to reect the consensus. The diculty is that processors can fail in arbitrary, unpredictable ways and can upset the consensus by communicating one clock value to one processor and a dierent clock value to another. An algorithm that can cope with such failures is said to be Byzantine fault-tolerant [LSP82]. There are a number of known algorithms for Byzantine fault-tolerant clock synchronization. These algorithms themselves are fairly simple to describe, but the reasoning required to establish their correctness is extremely delicate. The diculty stems from having to simultaneously deal with relative and absolute clock drifts, processor failures, reading errors, and the complicated arithmetic that is involved. Correctly modelling the behavior of clocks can itself be a dicult problem under these conditions. Schneider [Sch87] presents a clock synchronization scheme (abbreviated here as SCS) that captures the mathematics behind a number of individual synchronization algorithms. His scheme alleviates some of the complexity of reasoning about these protocols. Schneider regards each processor as maintaining a local clock by periodically adjusting its value to one computed by aconvergence function applied to the readings of all of the clocks. Schneider places certain natural conditions on the behavior of suitable convergence functions and shows that these conditions are sucient for demonstrating that at any time, the readings of two nonfaulty clocks are always within a xed bound of each other. The convergence functions used by individual protocols can then be shown to meet Schneider's conditions. The generality of Schneider's formulation made it an appropriate candidate for mechanical verication. Our verication employed the Ehdm specication/verication environment developed at the Computer Science Laboratory of SRI International. The verication provides a rigorous formalization of the behavior of clocks in the presence of Byzantine faults, and careful and tight derivations of the conditions needed to achieve synchronization. The use of Ehdm led to the 2
3 clarication of a number of details from Schneider's original presentation. For instance, Schneider employs a monotonicity condition on convergence functions that was found to be inessential for the proof. The monotonicity condition actually fails for several protocols (see Section 5). The mechanized proof clears up some minor inaccuracies in Schneider's derivation of several of the inequality constraints on the various quantities. The powerful decision procedures for linear equalities and inequalities provided by Ehdm were extremely useful for this proof. There are some other related eorts aimed at mechanically verifying distributed protocols. Rushby and von Henke [RvH91] have used Ehdm to check the proofs of Lamport and Melliar-Smith's interactive convergence clock synchronization algorithm (ICA) [LMS85]. This verication followed the original presentation of ICA in modelling local clocks as mapping clock time to real time. Our verication formalizes clocks as mapping real time to clock time. We compare these approaches in Section 6. Rushby [Rus91] uses Ehdm to model and verify fault masking and recovery in a synchronous N-plex system for fault-tolerance. Bevier and Young [BY90] have used the Boyer-Moore theorem prover to verify the Oral Messages algorithm for Byzantine agreement [LSP82] assuming that the processors are already synchronized. Schneider's results appear in a technical report and have not had the benet of widespread scrutiny so it is not surprising that errors were discovered during verication. On the other hand, the interactive convergence algorithm appears in a widely read journal paper [LMS85] and the verication attempt by Rushby and von Henke [RvH91] discovered aws in the proof that had, till then, safely survived the social process. The above machine-assisted proofs of distributed protocols were formalized in general-purpose logics. Ehdm, for example, uses a simply typed higher-order logic. Despite the mechanical assistance and the relative abstractness of the SCS protocol, our verication still required a signicant amount of eort. It is an interesting challenge to devise a logic that is more specialized to the task of describing faulttolerant distributed protocols and proving their correctness. In this paper, we describe one outcome of our mechanized verication, namely, a precise description of Schneider's clock synchronization scheme. We also examine the issues relating to the formal description and verication of such protocols. In Section 2 we discuss the problem of Byzantine fault-tolerant clock synchronization. Section 3 is a careful outline of the SCS protocol as rened by the mechanized verication. Section 4 is a brief sketch of the proof that was mechanically checked. Section 5 illustrates how the egocentric mean function of the ICA protocol satises Schneider's conditions. Some observations on the proof are presented in Section 6. The Appendices present the informal proof and some highlights of the mechanized verication. An expanded description of the proof is available as a technical report [Sha91]. 3
4 2 Byzantine Fault-tolerant Clock Synchronization In any implementation of synchronized clocks, each processor has a physical clock that is typically a crystal clock. Such aphysical clock drifts away from the xed standard time (\real time") at a rate that can be bounded. By periodically applying an adjustment to the reading of the physical clock, each processor also maintains a logical, or virtual, clock. The adjustment is computed by a protocol involving the exchange of clock readings by the various processors. The primary requirement that any algorithm for clock synchronization must satisfy is that at any instant, the absolute dierence, or the skew, between two virtual clock readings should be within some xed, acceptable bound. Processor failure adds a signicant dimension of complexity to the problem of clock synchronization. As an illustration of the diculty of synchronizing clocks in the presence of Byzantine failures, consider the case of three clocks a, b, and c, where only c is faulty, and nonfaulty clocks can gain or lose up to one minute during an hour. This means that two nonfaulty clocks could drift apart by two minutes over an hour since one clock can gain a minute while the other loses a minute. Suppose that the goal is to keep the nonfaulty clocks synchronized to within three minutes, where clock a gains a minute each hour and b loses a minute each hour. The clocks start synchronized at 12 noon. At 1pm, clock a reads 1:01pm, clock b reads 12:59pm, and clock c has failed. The clocks exchange their readings, and c maliciously communicates its reading as 1:03pm to a and as 12:57pm to b. At this point, a natural way for a clock to resynchronize would be to reset itself to the average of the acceptable clock readings, namely those readings that are within three minutes of its own reading. Then a resets itself to 1:01pm and b resets itself to 12:59pm, so that they remain two minutes apart. Continuing thus, at 2pm, clock a reads 2:02pm whereas clock b reads 1:58pm. The clocks a and b are now four minutes apart, thereby exceeding the acceptable bound on the skew between nonfaulty clocks. The above scenario illustrates one of the early clock synchronization protocols capable of tolerating Byzantine processor failures: the Interactive Convergence Algorithm (ICA) of Lamport and Melliar-Smith [LMS85]. ICA tolerates up to F failures for N processors where 3F < N, so that in the above case, at least four clocks are needed to tolerate a single failure. In ICA, a processor p resynchronizes for the i'th time when its clock reads ir. Processor p then reads the dierence between the other clock readings and its own clock reading. By ignoring clock readings that dier from its own by more than a certain xed value, a processor p computes the egocentric mean of the remaining clock readings as the required resynchronized clock reading. A number of functions can be used in place of egocentric mean function in order to compute the correction. For example, the fault-tolerant mean function takes the average of the clock readings that remain after the top F and the bottom F readings are discarded [LL84]. 4
5 The following section describes the formalization of the SCS protocol arising from our verication. 3 Schneider's Schema for Clock Synchronization The SCS protocol is described below in careful detail so that it can be compared with Schneider's original presentation [Sch87]. Section 3.1 describes how the logical clock is computed from the physical clock using the convergence function. Section 3.2 describes Schneider's conditions on the behavior of clocks and on suitable convergence functions. Note that we only deal with the case when the clocks are resynchronized with an instantaneous adjustment, whereas Schneider also deals with the situation when the adjustment is applied in a continuous manner. Since certain \clock ticks" might be lost or repeated in an instantaneous resynchronization, no critical events can be scheduled for these clock ticks. Another point to note is that both real time and clock readings range over real numbers in the formalization below, but the machine verication has also been carried out with natural number values for the time parameters. 3.1 Dening Clocks The physical and logical clocks are presented as functions from real time (as given by some external standard) to clock readings. This real time thus forms the frame of reference and is often referred to simply as \time." The variable t ranges over this real time. Values ranging over real time are written in lower case and clock times are in upper case. Synchronization takes place in rounds. The time at which processor p adjusts its clock following the i'th round of synchronization is represented by t i p. The starting time t 0 p is taken to be zero. PC p (t) is the reading of p's physical clock at real time t, and VC p (t)is p's virtual or logical clock reading. The virtual clock reading at time t i p is computed by applying an adjustment adj i p to the physical clock reading PC p (t i p). In its i'th, the virtual clock reading, VC p (t) and ti+1 p is interval of operation, i.e., when t i p t<ti+1 p is given by PC p (t)+adj i p. The virtual clock in the interval between ti p modelled by an abstraction called the interval clock whose value at time t is IC i p(t). At round 0, the adjustment adj 0 p is taken to be 0 so that for t<t 1 p, the reading VC p (t) is just PC p (t). For i>0, we let i p be an array of clock readings so that i p(q) isp's reading of ICq i,1 (t i p), i.e., q's (i, 1)'th interval clock reading at time t i p, since p is really estimating q's clock reading without taking into account the adjustment adj i q. The corrected value of the clock at time t i p, namely VC p (t i p), is computed by aconvergence function, cfn(p; i p). 1 1 In the Ehdm formalization, the array of observed clock readings i p, is actually represented as a function from clocks to readings. Since i p is a function, cfn is a higher-order function. 5
6 The above description leads to following denitions where i ranges over the natural numbers and t>0. adj i+1 p = cfn(p; i+1 p ), PC p (t i+1 p ) (3.1) adj 0 p = 0 (3.2) IC i p(t) = PC p (t)+adj i p (3.3) VC p (t) = IC i p(t); for t i p t<ti+1 p (3.4) It is easy to derive the following from Denitions (3.1), (3.3), and (3.4). VC p (t i+1 p ) = IC i+1 p (t i+1 p )=cfn(p; i+1 p ) (3.5) IC i+1 p (t) = cfn(p; i+1 p )+PC p (t), PC p (t i+1 p ) (3.6) In the next section, we enumerate the constraints on these quantities when p is a nonfaulty processor. The constraints on the behavior of the convergence function are particularly signicant. The main result obtained from these constraints and the above denitions is a bound on the skew between the logical clocks of two correct processors p and q. Theorem 3.1 (bounded skew) For any two clocks p and q that are nonfaulty at time t, jvc p (t),vc q (t)j (3:7) The proof of Theorem 3.1 is outlined in Section Clock conditions In formalizing the laws constraining the behavior of individual clocks, we must ensure that no assumptions are made regarding the faulty clocks since we are dealing with Byzantine failures. These laws which are conditions on the behavior of clocks are enumerated below. Individual protocols and clock implementations are expected to satisfy these conditions. Note that N is the total number of processors, and F is the maximum number of faulty clocks that the algorithm is expected to tolerate. To start, the following condition asserts that the nonfaulty clocks are synchronized to within the quantity S at time 0. Condition 1 (initial skew) For nonfaulty processors p and q jpc p (0), PC q (0)j S (3:8) The nonfaulty physical clocks must keep good enough time so that they do not drift away from real time by a rate greater than. Condition 2 (bounded drift) If clock p is nonfaulty at time s, s t, then (1, )(s, t) PC p (s),pc p (t) (1 + )(s, t) (3:9) 6
7 A useful corollary to bounded drift is that two physical clocks p and q that are not faulty 2 at time s, for s t, can drift further apart over the interval s, t by 2(s, t), since both p and q can drift by (s, t) with respect to real time, but in opposite directions. jpc p (s),pc q (s)jjpc p (t), PC q (t)j+2(s,t) (3:10) Each protocol has some mechanism for triggering the resynchronization of the clocks. Schneider postulates the existence of a global synchronization signal, t i G, which occurs at a period bounded from above and below. Our description dispenses with the notion of a global synchronization signal and bounds the period between the local synchronization signals and the range within which these signals occur. Condition 3 (bounded interval) For nonfaulty clock p 0 <r min t i+1 p, t i p r max (3:11) Condition 4 (bounded delay) For nonfaulty clocks p and q 3 jt i q, ti pj (3:12) Condition 5 (initial synchronization) For nonfaulty clock p t 0 p =0 (3:13) The following condition ensures that there is no overlap between synchronization periods, i.e., by the time any nonfaulty processor is ready to synchronize for the (i + 1)'th time, all nonfaulty processors have already synchronized for the i'th time. Condition 6 (nonoverlap) r min (3:14) An important corollary of the bounded interval and bounded delay conditions is that for any two nonfaulty clocks p and q, 0 t i+1 p, t i q r max + : (3:15) For a nonfaulty clock p, the value i+1 p (q) represents p's observation of q's i'th clock reading at time t i+1 p, i.e., itisp's estimate of IC i q(t i+1 p ). The error in this reading is assumed to be bounded by. 2 In the mechanized verication, great pains are taken to indicate the times at which the clocks are required to be nonfaulty. The informal discussion here makes the simplifying assumption that clocks are either faulty or nonfaulty, and often disregards the time at which clocks are asserted as being nonfaulty. 3 Rushby [private communication] observes that this condition is a somewhat stringent one since for most protocols, it entails the assumption that the clocks are already synchronized. This is an important observation since it implies that the demonstration that a particular protocol meets this condition will have to be carried out by induction over the number of synchronization rounds. 7
8 Condition 7 (reading error) For nonfaulty clocks p and q, jic i q(t i+1 p ), i+1 p (q)j (3:16) Condition 8 (bounded faults) At any time t, at most F processors are faulty. If p is nonfaulty at time t, then it is nonfaulty at any time s prior to t. The conditions below are mathematical constraints placed on the convergence function, e.g., clocks, drifts, and failures, do not play any role in the statements. The isolation of these constraints makes it possible to demonstrate that the egocentric mean function of ICA satises the conditions below independent of the context of its use. The condition of translation invariance indicates that adding x to the value of the convergence function should be the same as adding x to each clock reading instead. Condition 9 (translation invariance) For any function mapping clocks to clock values, cfn(p; (n: (n) + x)) = cfn(p; )+ x (3:17) The next condition of precision enhancement facilitates a comparison between values of the convergence function based on the range of values of some subset C of the clock readings. C is to be intuitively interpreted as the subset of nonfaulty processors. Precision enhancement captures the convergence behavior of the convergence function by asserting that the \closer" two arrays of clock readings and are to each other, the closer are the results of the convergence function applied to and, respectively. In the statement of precision enhancement, the above intuitive interpretation of C as the subset of nonfaulty clocks is permissible by the bounded faults condition. The \closeness" of and is formalized by asserting that all the readings in and, respectively, of clocks in C lie in an interval of width y, and that the corresponding readings of and of any clock incare no more than x apart. The function (x; y) captures the closeness of the values that result from applying the convergence function to and. 4 Condition 10 (precision enhancement) Given any subset C of the N clocks with jcj N,F, and clocks p and q in C, then for any readings and satisfying the conditions 1. for any l in C, j(l), (l)j x 2. for any l, m in C, j(l), (m)j y 3. for any l, m in C, j(l), (m)j y 4 Note that the order of arguments to are reversed from their order in Schneider's description [Sch87]. 8
9 there is a bound (x; y), such that jcfn(p; ), cfn(q; )j (x; y) (3:18) The nal condition of accuracy preservation bounds the distance between the value of cfn(p; ) and the nonfaulty readings in. 5 Condition 11 (accuracy preservation) Given any subset C of the N clocks with jcj N, F, and clock readings such that for any l and m in C, the bound j(l), (m)j xholds, there isabound (x) such that for any q in C jcfn(p; ), (q)j (x) (3:19) Schneider also proposes a condition called monotonicity that is actually not satised by several clock synchronization protocols though it is used heavily in Schneider's proofs. Fortunately, this condition turns out to be unnecessary in the derivation. The monotonicity condition asserts that if for each processor l, (l) (l), then cfn(p; ) cfn(p; ). The failure of the monotonicity condition for ICA is demonstrated in Section 5. 4 The Correctness Proof The formal arguments are extremely delicate to carry out carefully and correctly due to the additional consideration of processor failure. The phenomenon of processor failure is usually dealt with casually in informal presentations, but adds signicantly to the complexity of the formalization as well as the proof. A brief sketch of the proof is given below, and a few further details are provided in Appendix A. To establish the main result, Theorem 3.1, we must show that the skew, or absolute dierence, between the readings of any two nonfaulty clocks p and q at time t, given by jvc p (t),vc q (t)j, is bounded by a quantity. The rst step (Theorem 4.1) is to bound the skew at the instant when both p and q have resynchronized their clocks for the i'th time. This time, t i p;q, ismax(t i p ;ti q). The skew at this instant can be bounded by a quantity S that can be computed using the conditions of translation invariance, precision enhancement, and reading error, and the proof is by induction on i. Theorem 4.1 There isabound S such that for synchronization round i and any two nonfaulty processors p and q jic i p(t i p;q), IC i q(t i p;q)j S (4:20) 5 Footnote 7 in Schneider [Sch87] explains the choice of the terms precision enhancement and accuracy preservation. `Precision' is dened as the closeness with which a measurement can be reproduced, whereas `accuracy' is the proximity of the measurement to the actual value being measured. The virtual clocks represent various measurements of real time. Precision enhancement characterizes the closeness of these measurements to each other. Accuracy preservation can be seen as bounding the drift rate of the virtual clock with respect to real time. 9
10 We can now compute the quantity that bounds the skew in the interval t i p;q t < ti+1 p;q. The proof of Theorem 4.2 has two cases according to whether t < min(t i+1 p ;t i+1 q )ortmin(t i+1 p ;t i+1 q ). The rst case follows easily from bounded drift and bounded interval, and the second case requires accuracy preservation as well. Theorem 4.2 For any two nonfaulty clocks p, q, and t i p;q t<ti+1 p;q, jvc p (t),vc q (t)j: (4:21) Note that for any t 0, there is an i such that t<t i p;q. The main theorem then follows from the fact that Theorem 4.2 yields a skew bound for any t such that 0 t<t i p;q. We note of the various constraints on and S that arise from the proofs in Appendix A: 1. (2 + 2; S +2(r max + ) + 2) S 2. S +2r max 3. ( S +2(r max + ) + 2) ICA as an instance of Schneider's scheme To gain some intuition into the SCS protocol, we demonstrate that the egocentric mean function from the Interactive Convergence Algorithm of Lamport and Melliar- Smith [LMS85] satises Schneider's conditions of translation invariance, precision enhancement, and accuracy preservation. With the interactive convergence algorithm, the convergence function cfn I takes the egocentric mean of p's estimate of the readings of the N clocks numbered from 0toN,1, i.e., any readings that are more than away from p's own reading are replaced by p's own reading. This yields the denition where cfn I (p; ) = fix p (x)= ( x (p) P N,1 l=0 fix p((l)) N if jx, (p)j otherwise. Translation invariance follows from the observation that (5:22) fix p ((l: (l)+t)(q)) = fix p ((q)) + t (5:23) and P N,1 l=0 ((l)+t) N = P N,1 ((l)) l=0 + t (5:24) N 10
11 To demonstrate precision enhancement, we start with a set of processors C of cardinality jcj greater than N, F. Let f be N,jCj. The hypotheses for precision enhancement are that for any l and m in C, j(l), (l)j is bounded by x, and j(l), (m)j and j(l), (m)j are bounded by y. When y, it can be shown that jcfn I (p; ), cfn I (q; (N,f)x 2f+fx +fy )j + : (5:25) N N The right-hand side of (5.25) is the required (x; y) in this case. In the typical situation when the egocentric mean is computed, the quantity x representing the reading error is negligible, and y representing the clock skew is bounded by. Since the skew following synchronization should be smaller than, we can see that in Equation (5.25), the number of failed processors f should be below N=3. The derivation of (x; y) for the case when y>, is carried out in the mechanized proof. To show that cfn I satises accuracy preservation, it is sucient to observe that if all the clocks in C (the C-clocks) are within x of each other, then the C-clocks can cause the egocentric mean to be at most (N, f)x=n away from any nonfaulty clock. The clocks outside C can cause the egocentric mean to be up to f (x +)=N away from a good clock. The total thus yields (x) =x+ f N : The nal step is to demonstrate the failure of the monotonicity condition for ICA. The monotonicity condition mentioned at the end of Section 3.2 asserts that if for each processor l, (l) (l), then cfn(p; ) cfn(p; ). Let (p) = (p). Observe now that if there is some l such that (l)+ <(p), but with (p) >(l)(p),, then fix p ((l)) >fix p ((l)) holds. So, it is possible to have fix p ((l)) >fix p ((l)), even though we have (l)<(l). 6 Discussion The formal verication of the proof of the SCS protocol required considerable eort. Our own experience suggests that the diculty would have been comparable using other verication systems. The following discussion highlights some of the complexity of reasoning about fault-tolerant clock synchronization protocols, and examines some issues that are relevant to managing this complexity. Formalization itself is one source of complexity. Anumber of issues are simply swept under the rug in informal descriptions. For example, informal presentations of fault-tolerant protocols treat failure in a somewhat casual way. Clocks that fail are regarded as always having been faulty. Note that our informal presentation above makes essentially the same simplifying assumption. The mechanized proof is a great deal more precise. Clocks are allowed to fail at any point in time. A great 11
12 deal of care is taken to not build in any assumptions regarding the behavior of failed clocks save that their clock readings are unspecied functions of the standard global time. Under the assumption that clocks can fail at any time, the precise forms of the axioms are considerably more dicult to formulate. For example, the axioms rts0 and rts1 in Figure 2 are not at all the obvious formulations of the condition of bounded interval since p is constrained to be correct at time t. The obvious form of these axioms would assert p to be correct at t i+1 p and would thus say little about time points other than t i p and ti+1 p. We initially employed the \obvious" forms of these axioms and quickly found them inadequate during the course of the mechanized proof. These two axioms turned out to have some other inadequate variations as well. Other axioms formalizing clock behavior also posed similar challenges. Clock drifts are another obvious and inherent source of diculty in the proof. Virtually the entire proof consists of determining real time bounds on certain intervals and using these to derive bounds on the clock drifts over these intervals. The algebra involved in these calculations is very complex and has to be done with some care. It is conceivable that these calculations could be further automated so that these bounds can be computed rather than supplied by the user. A key dierence between our proof of the SCS protocol and the Rushby/von Henke proof of the ICA protocol is that they follow Lamport and Melliar-Smith in formalizing local clocks as functions from clock time to real time whereas local clocks are formalized here as functions from real time to clock time. As a consequence, our main theorem asserts that the skew between any two correct clocks at the same time instant is bounded, whereas their main theorem asserts a bound in the real time interval separating one correct clock's reading of time T from another correct clock's reading of time T.Wewere unable to conclusively establish either approach to be clearly superior. It seems likely that the best approach would be to simultaneously employ both notions of a local clock. The internal behavior of the each processor is governed by the local clock, and this can be mapped to its real time behavior. The synchronization between various processors is best done in terms of a real time frame of reference and subsequently mapped back to timing requirements on the behavior of the individual processors. The proofs here use a dense notion of time; the time variables range over ordered elds. The proof has been carried out with very minor changes with respect to a discrete notion of time. One signicant point ignored by the formalization here is that the bounded drift axiom can only be guaranteed to hold over a large enough interval of measurement. It would be easy to incorporate such a notion into the formalization and redo the proof. (The ability to easily redo proofs with minor perturbations to the assumptions is one of the signicant benets of mechanized formal verication.) Though there are a number of variants of temporal logic [Pnu77] that capture real-time notions [AH89, EMSS89, Koy89], none of these seem adequately sophisticated for dealing with faults and local clocks with any special felicity. It appears 12
13 that what is required of such a logic is the ability to easily translate from local time to global time assertions, to treat faultiness as a time-varying property, and to reason about the cardinalities of processors satisfying certain constraints. We are currently investigating the design of such a logic. It would also be interesting to examine whether the model-checking approaches [CG87] to the verication of distributed protocols can be fruitfully applied here. 7 Conclusions Rigorously proving the correctness of distributed protocols is an extremely dicult task, with or without mechanical assistance. Fault-tolerant clock synchronization is an excellent example of a problem where the algorithms, though often simple, are not at all easily veried. In such cases, it is extremely important tohave certain organizing principles which capture the common features of the various protocols with convincing generality. Schneider's schema for Byzantine clock synchronization provides such principles. The formalization here revises Schneider's presentation in some small ways. Schneider's notion of a global signal to trigger resynchronization has been dropped because such a notion is dicult to instantiate for many protocols. Though the quantities r max and r min have a dierent meaning from Schneider's, these dierences ought not to matter in any of the bounds derived. The derivation we present is extremely tight, given the structure of the proof. Schneider's monotonicity condition is avoided the proofs here. This condition is used heavily by Schneider in his arguments, but it actually turns out to not hold for many protocols. The statement of accuracy preservation here is also slightly dierent here from that of Schneider. The initial proof using Ehdm and including the pencil-and-paper development took about a month. The conditions on clocks and convergence functions were fairly dicult to formalize due to the careful treatment of failure. Many of these statements were rened during the course of the proof. The proof itself has been considerably revised and improved since the rst eort. Verifying that the egocentric mean function of ICA satised the conditions of translation invariance, accuracy preservation, and precision enhancement, took about two weeks. The complete proof involves about 182 theorems or lemmas. The most useful feature of Ehdm for this proof were the decision procedures for linear integer and rational inequalities and equalities. The proof is of course replete with long chains of inequality reasoning, and the decision procedures handled those steps in a fairly mechanical manner. The higher-order features of the language were also used to formalize the conditions of translation invariance, precision enhancement, and accuracy preservation, but such features were not essential to this proof. Fault-tolerant distributed protocols are suciently delicate to warrant careful, formal, mechanized analysis. Such an analysis is possible with the existing tech- 13
14 nology for specication and verication. Schneider's presentation provides a valuable mathematical framework for the verication of synchronization protocols. The machine-checked proof of Schneider's protocol led to a precise formulation of the protocol and a closely reasoned proof. It is inconceivable that the same degree of logical rigor and preciseness could be achieved without computational assistance. References [AH89] R. Alur and T. A. Henzinger. A really temporal logic. In 30th IEEE Symposium on Foundations of Computer Science, pages 164{169, [BY90] W. R. Bevier and W. D. Young. Machine checked proofs of the design and implementation of a fault-tolerant circuit. NASA Contractor Report , Computational Logic, Inc., [CG87] E. M. Clarke and O. Grumberg. Research on automatic verication of nite state concurrent systems. In Annual Review of Computer Science, pages 269{290. Annual Reviews, Inc., [EMSS89] E. A. Emerson, A. K. Mok, A. P. Sistla, and J. Srinivasan. Quantitative temporal reasoning. In Computer-Aided Verication, [Koy89] [LL84] [LMS85] R. Koymans. Speciying message passing and time-critical systems with temporal logic. PhD thesis, Eindhoven Univ. of Technology, J. Lundelius and N. A. Lynch. A new fault-tolerant algorithm for clock synchronization. In Proc. of the Third ACM Symp. on Principles of Distributed Computing, pages 75{88, L. Lamport and P. M. Melliar-Smith. Synchronizing clocks in the presence of faults. Journal of the ACM, 32(1):52{78, January [LSP82] Leslie Lamport, Robert Shostak, and Marshall Pease. The Byzantine generals problem. ACM Transactions on Programming Languages and Systems, 4(3):382{401, July [Pnu77] A. Pnueli. The temporal logic of programs. In Proc. 18th Ann. IEEE Symp. on Foundations of Computer Science, pages 46{57, [Rus91] John Rushby. Formal specication and verication of a fault-masking and transient-recovery model for digital ight-control systems. Technical Report SRI-CSL-91-3, Computer Science Laboratory, SRI International, Menlo Park, CA, January Also available as NASA Contractor Report 4384, July
15 [RvH91] John Rushby and Friedrich von Henke. Formal verication of the Interactive Convergence clock synchronization algorithm using Ehdm. Technical Report SRI-CSL-89-3R, Computer Science Laboratory, SRI International, Menlo Park, CA, February 1989 (Revised August 1991). Original version also available as NASA Contractor Report 4239, June [RvHO91] John Rushby, Friedrich von Henke, and Sam Owre. An introduction to formal specication and verication using Ehdm. Technical Report SRI-CSL-91-2, Computer Science Laboratory, SRI International, Menlo Park, CA, February [Sch87] Fred B. Schneider. Understanding protocols for Byzantine clock synchronization. Technical Report , Department of Computer Science, Cornell University, Ithaca, NY, August [Sha91] Natarajan Shankar. Mechanical verication of a schematic Byzantine fault-tolerant clock synchronization algorithm. Technical Report SRI- CSL-91-4, Computer Science Laboratory, SRI International, Menlo Park, CA, January Also available as NASA Contractor Report 4386, July
16 A Details of the Correctness Proof The details of the proof of bounded skew are completed below by providing the proofs of Theorems 4.1 and 4.2. Proof of Theorem 4.1. The proof is by induction on the round number i. Base case: When i =0,by (3.13) we havet 0 p=t 0 q= 0. The skew bound of S follows from Denitions (3.3) and (3.1), and the initial skew condition. Induction case: The induction hypothesis asserts that for every pair of nonfaulty processors, l and m jicl(t i i l;m), ICm(t i i l;m)j S (A:26) The goal is to establish for any pair of nonfaulty processors p and q, that jic i+1 p (t i+1 p;q ), IC i+1 q (t i+1 p;q )j S (A:27) Without loss of generality, assume that t i+1 q precedes t i+1 p so that t i+1 p;q = t i+1 p. Then Equation (3.6) and translation invariance yield IC i+1 q (t i+1 p ) = cfn(q; i+1 q )+PC q (t i+1 p ), PC q (t i+1 q ) By Equation (3.5), we have so that the required skew can be rewritten as = cfn(q; (n: i+1 q (n)+pc q (t i+1 p ), PC q (t i+1 q ))) (A.28) IC i+1 p (t i+1 p )=cfn(p; i+1 p ) (A:29) jcfn(q; (n: i+1 q (n)+pc q (t i+1 p ), PC q (t i+1 q ))), cfn(p; i+1 p )j This quantity can be bounded using precision enhancement with (n: i+1 q (n) + PC q (t i+1 p ),PC q (t i+1 q )) for and i+1 p for. The set C in precision enhancement is taken to be the subset of nonfaulty clocks as permitted by bounded faults. To satisfy Hypothesis 1 of precision enhancement, we need an x such that for any nonfaulty l, j( i+1 q (l)+pc q (t i+1 p ), PC q (t i+1 q )), i+1 p (l)j x: The value can be substituted for x since by bounded drift, j(pc q (t i+1 p ), PC q (t i+1 q )), (t i+1 p, t i+1 q )j (A:30) and by reading error and bounded drift, we get j( i+1 p (l), i+1 q (l)), (t i+1 p, t i+1 q )j 2 + j(ic i l (ti+1 p ), IC i l (ti+1 q )), (t i+1 p, t i+1 q )j 16
17 2 + (A.31) The induction hypothesis is needed in order to satisfy Hypotheses 2 and 3 of the relevant instance of precision enhancement. For both hypotheses, we need a y such that for any nonfaulty processors k, l and m, j i+1 k (l), i+1 k (m)j y (A:32) By reading error, the induction hypothesis (A.26), and Equations (3.15) and (3.10), we have j i+1 k (l), i+1 k (m)j 2 + jic i l(t i+1 k ), IC i m(t i+1 k )j 2 + jic i l(t i l;m), IC i m(t i l;m)j +2(t i+1 k, t i l;m) 2 + S +2(r max + ) (A.33) so that the required y is S +2(r max + ) + 2. So by precision enhancement, if (2 + 2; S +2(r max + ) + 2) S ; (A:34) then thus completing the proof of Theorem 4.1. jic i+1 p (t i+1 p ), IC i+1 q (t i+1 p )j S (A:35) Proof of Theorem 4.2. Assume without loss of generality that t i+1 q t i+1 p proof has two cases according to whether t i p;q t<ti+1 q or t i+1 q t<t i+1 p.. The Case 1: Assuming t i p;q t < ti+1 q. From bounded interval we get t, t i p;q r max. By Equation (3.4), we get VC p (t)=ic i p(t) and VC q (t)=ic i q(t). Then by Equations (3.10), (3.3), and Theorem 4.1, jvc p (t),vc q (t)j jvc p (t i p;q), VC q (t i p;q)j +2r max S +2r max (A.36) The bound should therefore be chosen so that S +2r max : (A:37) Case 2: Assuming t i+1 q <t<t i+1 p;q. In this interval, VC q (t)=ic i+1 q (t), whereas VC p (t)=ic i p (t). The strategy here is to bound the skew at ti+1 q and then compute the additional quantity by which the clocks can drift apart in the given interval. By 17
18 Equations (3.5) and (3.4), we have jvc p (t i+1 q ), VC q (t i+1 q )j = jic i p(t i+1 q ), cfn(q; i+1 q )j: (A:38) By reading error and accuracy preservation, the quantity jic i p(t i+1 q ), cfn(q; i+1 q )j can by bound by (x) +, where for any pair of nonfaulty clocks l and m, j i+1 q (l), i+1 q (m)j x: (A:39) As already seen in the derivation of Equation (A.32), that (A.39) holds with S + 2(r max + )+2forx.We then have jv C p (t i+1 q ), VC q (t i+1 q )j ( S +2(r max + )+2)+: (A:40) We can now bound the skew over the interval t i+1 q t<t i+1 p,by observing that t i+1 p, t i+1 q by (3.12), and applying Equation (3.10) to derive the inequality, jvc p (t),vc q (t)j( S +2(r max + )+2)++2: Therefore has to be chosen to satisfy (A:41) ( S +2(r max + )+2)++2 : (A:42) Both cases of the proof of Theorem 4.2 have been completed. This concludes the informal presentation of the proof. B The EHDM Proof Highlights This section contains the Ehdm formalization of the conditions axiomatizing the behavior of clocks described in Section 3 and the statements of the key theorems. Figure 1 contains the type declarations for some of the variables and constants used in clockassumptions. The clockassumptions module makes use of the module arith, which contains the basic arithmetic facts, and countmod, which introduces a counting function. Nonfaultiness is expressed by the predicate correct. The axioms constraining the physical behavior of the clock appear in Figure 2. Since we require to not exceed S, the axiom init corresponds to initial skew. Axiom correct closed asserts that a failed processor never recovers (see bounded faults). Axioms rate 1 and rate 2 together express the bounded drift condition. The axioms rts0 and rts1 capture the bounded interval condition. These axioms look strange because the variable t, needed to properly capture the correctness condition, appears in them but not in bounded interval. Most of the obvious ways of stating these axioms are either too restrictive or wrong. The axiom rts2 captures bounded delay, and synctime 0 is just initial synchronization. The condition of nonoverlap appears as an antecedent to the concluding theorem rather than as an axiom. In the LaT E X format below, multiplication is represented by as well 18
19 clockassumptions: Module Using arith, countmod Exporting all with countmod, arith Theory process: Type is nat event: Type is nat time: Type is number Clocktime: Type is number l; m; n; p; q; p 1 ;p 2 ;q 1 ;q 2 ;p 3 ;q 3 : Var process i; j; k: Var event x; y; z; r;s;t: Var time X; Y; Z; R; S; T : Var Clocktime ; : Var function[process! Clocktime] ;;;r min ;r max ;;: number PC?1 (?2);VC?1 (?2): function[process, time! Clocktime] t?2?1: function[process, event! time]?2?1: function[process, event! function[process! Clocktime]] IC?2?1(?3): function[process, event, time! Clocktime] correct: function[process, time! bool] cfn: function[process, function[process! Clocktime]! Clocktime] : function[clocktime, Clocktime! Clocktime] : function[clocktime! Clocktime] Figure 1: Declarations from module clockassumptions as?. These are synonymous, but the latter represents the uninterpreted form of multiplication whereas the former is interpreted by the linear arithmetic decision procedures of Ehdm. The denitions of the virtual clock and the interval clock in terms of the physical clock appear in Figure 3. These correspond to (3.1), (3.4), and (3.3), respectively. The conditions on the convergence function appear in Figure 4. The axiom Readerror corresponds to the condition reading error. The axiom correct count corresponds to bounded faults. The remaining correspondences should be selfevident. The conclusion corresponding to Theorem 3.1 is the theorem agreement in Figure 5. The veried version of Theorem 4.1 is given in Figure 6, and that of Theorem 4.2 in Figure 7. The expression t i is an alternative notation for (p*q)[i] ti p;q since (p * q)[i] represents p if t i p ti q, and q otherwise. 19
20 init: Axiom correct(p; 0) PC p (0) 0 ^ PC p (0) correct closed: Axiom s t ^ correct(p; s) correct(p; t) rate 1: Axiom correct(p; s) ^ s t PC p (s),pc p (t) (s,t)?(1 + ) rate 2: Axiom correct(p; s) ^ s t PC p (s),pc p (t) (s,t)?(1, ) rts0: Axiom correct(p; t) ^ t t i+1 p rts1: Axiom correct(p; t) ^ t t i+1 p t, t i p r max t, t i p r min rts 0: Lemma correct(p; t i+1 p ) t i+1 p, t i p r max rts 1: Lemma correct(p; t i+1 p ) t i+1 p, t i p r min rts2: Axiom correct(p; t) ^ t t i q + ^ correct(q; t) t t i p rts 2: Axiom correct(p; t i p) ^ correct(q; t i q) t i p, t i q synctime 0: Axiom t 0 p =0 Figure 2: Physical clock axioms VClock defn: Axiom correct(p; t) ^ t t i p ^ t<ti+1 p VC p (t)=ic i p (t) Adj: function[process, event! Clocktime] = ( p;i:( if i>0then cfn(p; i p ), PC p(t i p ) else 0 end if)) IClock defn: Axiom correct(p; t) IC i p (t)=pc p(t) + Adj(p; i) Figure 3: Clock denitions 20
Computing for Critical Applications, Garmisch-Partenkirchen, Germany, March, 1997. Systematic Formal Verication for Fault-Tolerant.
Expanded version of a paper from the Sixth Working Conference on Dependable Computing for Critical Applications, Garmisch-Partenkirchen, Germany, March, 1997. IEEE Computer Society Press, pp. 203{222.More information
Ecient approximation algorithm for minimizing makespan. on uniformly related machines. Chandra Chekuri. November 25, 1997.
Ecient approximation algorithm for minimizing makespan on uniformly related machines Chandra Chekuri November 25, 1997 Abstract We obtain a new ecient approximation algorithm for scheduling precedenceMore information
An example of a computable
An example of a computable absolutely normal number Verónica Becher Santiago Figueira Abstract The first example of an absolutely normal number was given by Sierpinski in 96, twenty years before the conceptMore information
1.1 Related work For non-preemptive scheduling on uniformly related machines the rst algorithm with a constant competitive ratio was given by Aspnes e
A Lower Bound for On-Line Scheduling on Uniformly Related Machines Leah Epstein Jir Sgall September 23, 1999 email@example.com, Department of Computer Science, Tel-Aviv University, Israel; firstname.lastname@example.com,More information
The Generalized Railroad Crossing: A Case Study in Formal. Abstract
The Generalized Railroad Crossing: A Case Study in Formal Verication of Real-Time Systems Constance Heitmeyer Nancy Lynch y Abstract A new solution to the Generalized Railroad Crossing problem, based onMore information
Neeraj Suri, Michelle M. Hugue and Chris J. Walter. AlliedSignal Electronics & Technology Center. email: email@example.com.
Synchronization Issues in Real-Time Systems Neeraj Suri, Michelle M. Hugue and Chris J. Walter AlliedSignal Electronics & Technology Center 9140 Old Annapolis Road Columbia, MD 21045 email: email@example.com information
Bounded Cost Algorithms for Multivalued Consensus Using Binary Consensus Instances
Bounded Cost Algorithms for Multivalued Consensus Using Binary Consensus Instances Jialin Zhang Tsinghua University firstname.lastname@example.com Wei Chen Microsoft Research Asia firstname.lastname@example.com AbstractMore information
Verication by Finitary Abstraction Weizmann Institute of Sciences and Universite Joseph Fourier, Grenoble Fourth International Spin Workshop (SPIN'98) Paris 2.11.98 Joint work with: Y. Kesten Ben GurionMore information
Induction. Margaret M. Fleck. 10 October These notes cover mathematical induction and recursive definition
Induction Margaret M. Fleck 10 October 011 These notes cover mathematical induction and recursive definition 1 Introduction to induction At the start of the term, we saw the following formula for computingMore information
Time and Clocks. Time and Clocks. Time
Time and Clocks Time: we model the continuum of real-time as a directed timeline consisting of an infinite set {T} of instants with the following properties: {T} is an ordered set, i.e., if p and q areMore information
An Overview of Clock Synchronization
An Overview of Clock Synchronization Barbara Simons, IBM Almaden Research Center Jennifer Lundelius Welch, GTE Laboratories Incorporated Nancy Lynch, MIT 1 Introduction A distributed system consists ofMore information
Answer Key for California State Standards: Algebra I
Algebra I: Symbolic reasoning and calculations with symbols are central in algebra. Through the study of algebra, a student develops an understanding of the symbolic language of mathematics and the sciences.More information
A simple algorithm with no simple verication
A simple algorithm with no simple verication Laszlo Csirmaz Central European University Abstract The correctness of a simple sorting algorithm is resented, which algorithm is \evidently wrong" at the rstMore information
WHAT ARE MATHEMATICAL PROOFS AND WHY THEY ARE IMPORTANT? introduction Many students seem to have trouble with the notion of a mathematical proof. People that come to a course like Math 216, who certainlyMore information
CHAPTER 3. Methods of Proofs. 1. Logical Arguments and Formal Proofs
CHAPTER 3 Methods of Proofs 1. Logical Arguments and Formal Proofs 1.1. Basic Terminology. An axiom is a statement that is given to be true. A rule of inference is a logical rule that is used to deduceMore information
Continued Fractions and the Euclidean Algorithm
Continued Fractions and the Euclidean Algorithm Lecture notes prepared for MATH 326, Spring 997 Department of Mathematics and Statistics University at Albany William F Hammond Table of Contents IntroductionMore information
The Conference Call Search Problem in Wireless Networks
The Conference Call Search Problem in Wireless Networks Leah Epstein 1, and Asaf Levin 2 1 Department of Mathematics, University of Haifa, 31905 Haifa, Israel. firstname.lastname@example.com 2 Department of Statistics,More information
x if x 0, x if x < 0.
Chapter 3 Sequences In this chapter, we discuss sequences. We say what it means for a sequence to converge, and define the limit of a convergent sequence. We begin with some preliminary results about theMore information
Elementary Number Theory We begin with a bit of elementary number theory, which is concerned
CONSTRUCTION OF THE FINITE FIELDS Z p S. R. DOTY Elementary Number Theory We begin with a bit of elementary number theory, which is concerned solely with questions about the set of integers Z = {0, ±1,More information
The Trip Scheduling Problem
The Trip Scheduling Problem Claudia Archetti Department of Quantitative Methods, University of Brescia Contrada Santa Chiara 50, 25122 Brescia, Italy Martin Savelsbergh School of Industrial and SystemsMore information
Fall 2011. Andrew U. Frank, October 23, 2011
Fall 2011 Andrew U. Frank, October 23, 2011 TU Wien, Department of Geoinformation and Cartography, Gusshausstrasse 27-29/E127.1 A-1040 Vienna, Austria firstname.lastname@example.com Part I Introduction 1 TheMore information
A New, Publicly Veriable, Secret Sharing Scheme
Scientia Iranica, Vol. 15, No. 2, pp 246{251 c Sharif University of Technology, April 2008 A New, Publicly Veriable, Secret Sharing Scheme A. Behnad 1 and T. Eghlidos A Publicly Veriable Secret SharingMore information
Some Polynomial Theorems. John Kennedy Mathematics Department Santa Monica College 1900 Pico Blvd. Santa Monica, CA 90405 firstname.lastname@example.com.
Some Polynomial Theorems by John Kennedy Mathematics Department Santa Monica College 1900 Pico Blvd. Santa Monica, CA 90405 firstname.lastname@example.com This paper contains a collection of 31 theorems, lemmas,More information
Invertible elements in associates and semigroups. 1
Quasigroups and Related Systems 5 (1998), 53 68 Invertible elements in associates and semigroups. 1 Fedir Sokhatsky Abstract Some invertibility criteria of an element in associates, in particular in n-aryMore information
Problems Encountered in the Machine-assisted Proof of Hardware? Paul Curzon University of Cambridge Computer Laboratory, Pembroke Street, Cambridge, UK. Email: email@example.com URL http://www.cl.cam.ac.uk/users/pc/More information
CMSC 858T: Randomized Algorithms Spring 2003 Handout 8: The Local Lemma
CMSC 858T: Randomized Algorithms Spring 2003 Handout 8: The Local Lemma Please Note: The references at the end are given for extra reading if you are interested in exploring these ideas further. You areMore information
Scheduling Real-time Tasks: Algorithms and Complexity
Scheduling Real-time Tasks: Algorithms and Complexity Sanjoy Baruah The University of North Carolina at Chapel Hill Email: firstname.lastname@example.com Joël Goossens Université Libre de Bruxelles Email: firstname.lastname@example.com information
Thesis work and research project
Thesis work and research project Hélia Pouyllau, INRIA of Rennes, Campus Beaulieu 35042 Rennes, firstname.lastname@example.com July 16, 2007 1 Thesis work on Distributed algorithms for endto-end QoS contractMore information
Analysis of Load Frequency Control Performance Assessment Criteria
520 IEEE TRANSACTIONS ON POWER SYSTEMS, VOL. 16, NO. 3, AUGUST 2001 Analysis of Load Frequency Control Performance Assessment Criteria George Gross, Fellow, IEEE and Jeong Woo Lee Abstract This paper presentsMore information
Information Theory and Coding Prof. S. N. Merchant Department of Electrical Engineering Indian Institute of Technology, Bombay
Information Theory and Coding Prof. S. N. Merchant Department of Electrical Engineering Indian Institute of Technology, Bombay Lecture - 17 Shannon-Fano-Elias Coding and Introduction to Arithmetic CodingMore information
CHAPTER II THE LIMIT OF A SEQUENCE OF NUMBERS DEFINITION OF THE NUMBER e.
CHAPTER II THE LIMIT OF A SEQUENCE OF NUMBERS DEFINITION OF THE NUMBER e. This chapter contains the beginnings of the most important, and probably the most subtle, notion in mathematical analysis, i.e.,More information
Stochastic Inventory Control
Chapter 3 Stochastic Inventory Control 1 In this chapter, we consider in much greater details certain dynamic inventory control problems of the type already encountered in section 1.3. In addition to theMore information
Biinterpretability up to double jump in the degrees
Biinterpretability up to double jump in the degrees below 0 0 Richard A. Shore Department of Mathematics Cornell University Ithaca NY 14853 July 29, 2013 Abstract We prove that, for every z 0 0 with zMore information
Rigorous Software Development CSCI-GA 3033-009
Rigorous Software Development CSCI-GA 3033-009 Instructor: Thomas Wies Spring 2013 Lecture 11 Semantics of Programming Languages Denotational Semantics Meaning of a program is defined as the mathematicalMore information
Linear Programming Notes V Problem Transformations
Linear Programming Notes V Problem Transformations 1 Introduction Any linear programming problem can be rewritten in either of two standard forms. In the first form, the objective is to maximize, the materialMore information
Introducing Formal Methods. Software Engineering and Formal Methods
Introducing Formal Methods Formal Methods for Software Specification and Analysis: An Overview 1 Software Engineering and Formal Methods Every Software engineering methodology is based on a recommendedMore information
Topology-based network security
Topology-based network security Tiit Pikma Supervised by Vitaly Skachek Research Seminar in Cryptography University of Tartu, Spring 2013 1 Introduction In both wired and wireless networks, there is theMore information
Chapter 6: distributed systems
Chapter 6: distributed systems Strongly related to communication between processes is the issue of how processes in distributed systems synchronize. Synchronization is all about doing the right thing atMore information
SECURITY METRICS: MEASUREMENTS TO SUPPORT THE CONTINUED DEVELOPMENT OF INFORMATION SECURITY TECHNOLOGY Shirley Radack, Editor Computer Security Division Information Technology Laboratory National InstituteMore information
Clock Synchronization
Clock Synchronization Henrik Lönn Electronics & Software Volvo Technological Development Contents General Types of Synchronisation Faults and problems to cope with Example algorithms Transmission delaysMore information
Planning and Scheduling in the Digital Factory
Institute for Computer Science and Control Hungarian Academy of Sciences Berlin, May 7, 2014 1 Why "digital"? 2 Some Planning and Scheduling problems 3 Planning for "one-of-a-kind" products 4 SchedulingMore information
Distributed Synchronization
CIS 505: Software Systems Lecture Note on Physical Clocks Insup Lee Department of Computer and Information Science University of Pennsylvania Distributed Synchronization Communication between processesMore information
Discrete Mathematics and Probability Theory Fall 2009 Satish Rao, David Tse Note 2
CS 70 Discrete Mathematics and Probability Theory Fall 2009 Satish Rao, David Tse Note 2 Proofs Intuitively, the concept of proof should already be familiar We all like to assert things, and few of usMore information
3. Mathematical Induction
3. MATHEMATICAL INDUCTION 83 3. Mathematical Induction 3.1. First Principle of Mathematical Induction. Let P (n) be a predicate with domain of discourse (over) the natural numbers N = {0, 1,,...}. If (1)More information
Modern Optimization Methods for Big Data Problems MATH11146 The University of Edinburgh
Modern Optimization Methods for Big Data Problems MATH11146 The University of Edinburgh Peter Richtárik Week 3 Randomized Coordinate Descent With Arbitrary Sampling January 27, 2016 1 / 30 The ProblemMore information
Synchronization in. Distributed Systems. Cooperation and Coordination in. Distributed Systems. Kinds of Synchronization.
Cooperation and Coordination in Distributed Systems Communication Mechanisms for the communication between processes Naming for searching communication partners Synchronization in Distributed Systems But...More information
Week 5 Integral Polyhedra
Week 5 Integral Polyhedra We have seen some examples 1 of linear programming formulation that are integral, meaning that every basic feasible solution is an integral vector. This week we develop a theoryMore information
DEGREES OF ORDERS ON TORSION-FREE ABELIAN GROUPS ASHER M. KACH, KAREN LANGE, AND REED SOLOMON Abstract. We construct two computable presentations of computable torsion-free abelian groups, one of isomorphismMore information
1 if 1 x 0 1 if 0 x 1
Chapter 3 Continuity In this chapter we begin by defining the fundamental notion of continuity for real valued functions of a single real variable. When trying to decide whether a given function is orMore information
The Relation between Two Present Value Formulae
James Ciecka, Gary Skoog, and Gerald Martin. 009. The Relation between Two Present Value Formulae. Journal of Legal Economics 15(): pp. 61-74. The Relation between Two Present Value Formulae James E. Ciecka,More information
Notes from February 11
Notes from February 11 Math 130 Course web site: www.courses.fas.harvard.edu/5811 Two lemmas Before proving the theorem which was stated at the end of class on February 8, we begin with two lemmas. TheMore information
An improved on-line algorithm for scheduling on two unrestrictive parallel batch processing machines
This is the Pre-Published Version. An improved on-line algorithm for scheduling on two unrestrictive parallel batch processing machines Q.Q. Nong, T.C.E. Cheng, C.T. Ng Department of Mathematics, OceanMore information
NASA Technical Memorandum 108991 (Revised) An Elementary Tutorial on Formal. Specication and Verication. Using PVS 2. Ricky W.
NASA Technical Memorandum 108991 (Revised) An Elementary Tutorial on Formal Specication and Verication Using PVS 2 Ricky W. Butler September 1993 (revised June 1995) NASA National Aeronautics and SpaceMore information
Minimizing the Eect of Clock Skew. Via Circuit Retiming 1. Technical Report 93-5-04. May, 1992
Minimizing the Eect of Clock kew Via Circuit Retiming 1 Brian Lockyear and Carl Ebeling Department of Computer cience and Engineering University of Washington eattle, Washington 98195 Technical ReportMore information
Mathematical Reasoning in Software Engineering Education. Peter B. Henderson Butler University
Mathematical Reasoning in Software Engineering Education Peter B. Henderson Butler University Introduction Engineering is a bridge between science and mathematics, and the technological needs of mankind.More information
How to build a probability-free casino
How to build a probability-free casino Adam Chalcraft CCR La Jolla firstname.lastname@example.com Chris Freiling Cal State San Bernardino firstname.lastname@example.com Randall Dougherty CCR La Jolla email@example.com JasonMore information
Section 3 Sequences and Limits, Continued.
Section 3 Sequences and Limits, Continued. Lemma 3.6 Let {a n } n N be a convergent sequence for which a n 0 for all n N and it α 0. Then there exists N N such that for all n N. α a n 3 α In particularMore information
Combinatorial PCPs with ecient veriers
Combinatorial PCPs with ecient veriers Or Meir Abstract The PCP theorem asserts the existence of proofs that can be veried by a verier that reads only a very small part of the proof. The theorem was originallyMore information
Synchronization in Distributed Systems
Synchronization in Distributed Systems Chapter 4: Time and Synchronisation Page 1 1 Cooperation and Coordination in Distributed Systems Communication Mechanisms for the communication between processesMore information
Automated Theorem Proving - summary of lecture 1
Automated Theorem Proving - summary of lecture 1 1 Introduction Automated Theorem Proving (ATP) deals with the development of computer programs that show that some statement is a logical consequence ofMore information
MATH10212 Linear Algebra. Systems of Linear Equations. Definition. An n-dimensional vector is a row or a column of n numbers (or letters): a 1.
MATH10212 Linear Algebra Textbook: D. Poole, Linear Algebra: A Modern Introduction. Thompson, 2006. ISBN 0-534-40596-7. Systems of Linear Equations Definition. An n-dimensional vector is a row or a columnMore information
15.062 Data Mining: Algorithms and Applications Matrix Math Review
.6 Data Mining: Algorithms and Applications Matrix Math Review The purpose of this document is to give a brief review of selected linear algebra concepts that will be useful for the course and to developMore information
17.6.1 Introduction to Auction Design
CS787: Advanced Algorithms Topic: Sponsored Search Auction Design Presenter(s): Nilay, Srikrishna, Taedong 17.6.1 Introduction to Auction Design The Internet, which started of as a research project inMore information
There is no degree invariant half-jump
There is no degree invariant half-jump Rod Downey Mathematics Department Victoria University of Wellington P O Box 600 Wellington New Zealand Richard A. Shore Mathematics Department Cornell UniversityMore information
Query Order and NP-Completeness 1 Jack J.Dai Department of Mathematics Iowa State University Ames, Iowa 50011 U.S.A. Jack H.Lutz Department of Computer Science Iowa State University Ames, Iowa 50011 U.S.A.More information
Oscillations of the Sending Window in Compound TCP
Oscillations of the Sending Window in Compound TCP Alberto Blanc 1, Denis Collange 1, and Konstantin Avrachenkov 2 1 Orange Labs, 905 rue Albert Einstein, 06921 Sophia Antipolis, France 2 I.N.R.I.A. 2004More information
The Bakery Algorithm: Yet Another. Specication and Verication. Dean Rosenzweig z. Abstract. In a meeting at Schloss Dagstuhl in June 1993, Uri Abraham
1 The Bakery Algorithm: Yet Another Specication and Verication Egon Borger Yuri Gurevich y Dean Rosenzweig z Abstract In a meeting at Schloss Dagstuhl in June 1993, Uri Abraham and Menachem Magidor haveMore information
Homework 1 (Time, Synchronization and Global State) - 100 Points
Homework 1 (Time, Synchronization and Global State) - 100 Points CS25 Distributed Systems, Fall 2009, Instructor: Klara Nahrstedt Out: Thursday, September 3, Due Date: Thursday, September 17 Instructions:More information
Remarks on the GWV Firewall
Remarks on the GWV Firewall Ron van der Meyden School of Computer Science and Engineering, University of New South Wales October 18, 2010 Abstract Greve, Wilding and Vanfleet (2003) have proposed a formalMore information
The Epsilon-Delta Limit Definition:
The Epsilon-Delta Limit Definition: A Few Examples Nick Rauh 1. Prove that lim x a x 2 = a 2. (Since we leave a arbitrary, this is the same as showing x 2 is continuous.) Proof: Let > 0. We wish to findMore information
CHAPTER 3 Numbers and Numeral Systems
CHAPTER 3 Numbers and Numeral Systems Numbers play an important role in almost all areas of mathematics, not least in calculus. Virtually all calculus books contain a thorough description of the natural,More information
Chapter 7. Continuity
Chapter 7 Continuity There are many processes and eects that depends on certain set of variables in such a way that a small change in these variables acts as small change in the process. Changes of thisMore information
THE DIMENSION OF A VECTOR SPACE KEITH CONRAD This handout is a supplementary discussion leading up to the definition of dimension and some of its basic properties. Let V be a vector space over a fieldMore information
The rigorous development and verication of a boiler system specication is presented.
Stepwise Development and Verication of a Boiler System Specication Peter Bishop and Glenn Bruns and Stuart Anderson Abstract The rigorous development and verication of a boiler system specication is presented.More information
4.1 Introduction - Online Learning Model
Computational Learning Foundations Fall semester, 2010 Lecture 4: November 7, 2010 Lecturer: Yishay Mansour Scribes: Elad Liebman, Yuval Rochman & Allon Wagner 1 4.1 Introduction - Online Learning ModelMore information
Verifying Semantic of System Composition for an Aspect-Oriented Approach
2012 International Conference on System Engineering and Modeling (ICSEM 2012) IPCSIT vol. 34 (2012) (2012) IACSIT Press, Singapore Verifying Semantic of System Composition for an Aspect-Oriented ApproachMore information
School of Computer Science, Carnegie Mellon University, Pittsburgh, PA 15213
,, 1{8 () c A Note on Learning from Multiple-Instance Examples AVRIM BLUM email@example.com ADAM KALAI firstname.lastname@example.com School of Computer Science, Carnegie Mellon University, Pittsburgh, PA 1513 Abstract.More information
On Correlating Performance Metrics
On Correlating Performance Metrics Yiping Ding and Chris Thornley BMC Software, Inc. Kenneth Newman BMC Software, Inc. University of Massachusetts, Boston Performance metrics and their measurements areMore information
Jieh Hsiang Department of Computer Science State University of New York Stony brook, NY 11794
ASSOCIATIVE-COMMUTATIVE REWRITING* Nachum Dershowitz University of Illinois Urbana, IL 61801 N. Alan Josephson University of Illinois Urbana, IL 01801 Jieh Hsiang State University of New York Stony brook,More information
[Refer Slide Time: 05:10]
Principles of Programming Languages Prof: S. Arun Kumar Department of Computer Science and Engineering Indian Institute of Technology Delhi Lecture no 7 Lecture Title: Syntactic Classes Welcome to lectureMore information
Dynamic TCP Acknowledgement: Penalizing Long Delays
Dynamic TCP Acknowledgement: Penalizing Long Delays Karousatou Christina Network Algorithms June 8, 2010 Karousatou Christina (Network Algorithms) Dynamic TCP Acknowledgement June 8, 2010 1 / 63 LayoutMore information
(Refer Slide Time: 01:11-01:27)
Digital Signal Processing Prof. S. C. Dutta Roy Department of Electrical Engineering Indian Institute of Technology, Delhi Lecture - 6 Digital systems (contd.); inverse systems, stability, FIR and IIR,More information
11 Ideals. 11.1 Revisiting Z
11 Ideals The presentation here is somewhat different than the text. In particular, the sections do not match up. We have seen issues with the failure of unique factorization already, e.g., Z[ 5] = O Q(More information
The program also provides supplemental modules on topics in geometry and probability and statistics.
Algebra 1 Course Overview Students develop algebraic fluency by learning the skills needed to solve equations and perform important manipulations with numbers, variables, equations, and inequalities. StudentsMore information
International Journal of Information Technology, Modeling and Computing (IJITMC) Vol.1, No.3,August 2013
FACTORING CRYPTOSYSTEM MODULI WHEN THE CO-FACTORS DIFFERENCE IS BOUNDED Omar Akchiche 1 and Omar Khadir 2 1,2 Laboratory of Mathematics, Cryptography and Mechanics, Fstm, University of Hassan II Mohammedia-Casablanca,More information
Numerical Analysis Lecture Notes
Numerical Analysis Lecture Notes Peter J. Olver 5. Inner Products and Norms The norm of a vector is a measure of its size. Besides the familiar Euclidean norm based on the dot product, there are a numberMore information
Specification and Analysis of Contracts Lecture 1 Introduction
Specification and Analysis of Contracts Lecture 1 Introduction Gerardo Schneider email@example.com http://folk.uio.no/gerardo/ Department of Informatics, University of Oslo SEFM School, Oct. 27 - Nov.More information
Recent progress in additive prime number theory
Recent progress in additive prime number theory University of California, Los Angeles Mahler Lecture Series Additive prime number theory Additive prime number theory is the study of additive patterns inMore information
ON THE CONSEQUENCES OF THE STATISTICAL MECHANICS THEORY OF LEARNING CURVES FOR THE MODEL SELECTION PROBLEM 1. Introduction MICHAEL J. KEARNS AT&T BELL LABORATORIES Murray Hill, New Jersey 07974, USA E-mail:More information
Determination of the normalization level of database schemas through equivalence classes of attributes
Computer Science Journal of Moldova, vol.17, no.2(50), 2009 Determination of the normalization level of database schemas through equivalence classes of attributes Cotelea Vitalie Abstract In this paper,More information
Notes on Factoring. MA 206 Kurt Bryan
The General Approach Notes on Factoring MA 26 Kurt Bryan Suppose I hand you n, a 2 digit integer and tell you that n is composite, with smallest prime factor around 5 digits. Finding a nontrivial factorMore information
STRUTS: Statistical Rules of Thumb. Seattle, WA
STRUTS: Statistical Rules of Thumb Gerald van Belle Departments of Environmental Health and Biostatistics University ofwashington Seattle, WA 98195-4691 Steven P. Millard Probability, Statistics and InformationMore information
2.1 Complexity Classes
15-859(M): Randomized Algorithms Lecturer: Shuchi Chawla Topic: Complexity classes, Identity checking Date: September 15, 2004 Scribe: Andrew Gilpin 2.1 Complexity Classes In this lecture we will lookMore information
x 2 f 2 e 1 e 4 e 3 e 2 q f 4 x 4 f 3 x 3
Karl-Franzens-Universitat Graz & Technische Universitat Graz SPEZIALFORSCHUNGSBEREICH F 003 OPTIMIERUNG und KONTROLLE Projektbereich DISKRETE OPTIMIERUNG O. Aichholzer F. Aurenhammer R. Hainz New ResultsMore information
Many algorithms, particularly divide and conquer algorithms, have time complexities which are naturally
Recurrence Relations Many algorithms, particularly divide and conquer algorithms, have time complexities which are naturally modeled by recurrence relations. A recurrence relation is an equation whichMore information
a 11 x 1 + a 12 x 2 + + a 1n x n = b 1 a 21 x 1 + a 22 x 2 + + a 2n x n = b 2.
Chapter 1 LINEAR EQUATIONS 1.1 Introduction to linear equations A linear equation in n unknowns x 1, x,, x n is an equation of the form a 1 x 1 + a x + + a n x n = b, where a 1, a,..., a n, b are givenMore information
Chapter II. Controlling Cars on a Bridge
Chapter II. Controlling Cars on a Bridge 1 Introduction The intent of this chapter is to introduce a complete example of a small system development. During this development, you will be made aware of theMore information
An Eective Load Balancing Policy for
An Eective Load Balancing Policy for Geometric Decaying Algorithms Joseph Gil y Dept. of Computer Science The Technion, Israel Technion City, Haifa 32000 ISRAEL Yossi Matias z AT&T Bell Laboratories 600More information
A Systematic Approach. to Parallel Program Verication. Tadao TAKAOKA. Department of Computer Science. Ibaraki University. Hitachi, Ibaraki 316, JAPAN
A Systematic Approach to Parallel Program Verication Tadao TAKAOKA Department of Computer Science Ibaraki University Hitachi, Ibaraki 316, JAPAN E-mail: email@example.com Phone: +81 94 38 5130More information
Some other convex-valued selection theorems 147 (2) Every lower semicontinuous mapping F : X! IR such that for every x 2 X, F (x) is either convex and
PART B: RESULTS x1. CHARACTERIZATION OF NORMALITY- TYPE PROPERTIES 1. Some other convex-valued selection theorems In this section all multivalued mappings are assumed to have convex values in some BanachMore information


text:
Toggle navigation
Games List
Upload Games
November 4-6, 2016
5:30 Doors Open (with live music by Fat Bard), 6:00 Event Begins
WHERE? The Saint Louis Zoo
The Living World's Anheuser-Busch Theater at the Saint Louis Zoo
Map to The Saint Louis Zoo
Park at the North Parking lot and The Living World is just inside the Zoo's Entrance. The Anheuser-Busch Theater is on the first floor. Parking is Free for participants!
The theme is
"Open to Interpretation"
Ask Questions. Listen for announcements. Find Help. Join a team. Complain. Whatever.
Want to chat? Join us on Discord. It's free, and we've got a dedicated server for the event thanks to
Explore the Zoo
Make a game that explores the St. Louis Zoo! Consider using AR, VR, or Google Maps.
Go Green
Encourage saving the planet! Show off your ideas for alternative energy, bag/trash collection, or the recycling/reuse of products.
Save the Wild
Help bring awareness to endangered animals! Save, protect, or educate others about endangered animals.
Don't harm a hair on anybody's head! Try to make a game with absolutely no violence.
Fan of foreign cinema? Well now it's your turn to add subs, dubs, or references to other languages.
Battle Royale with Cheese
Make a game with multiplayer... And cheese!
Candy Coma
Make a game that clearly takes place right after Halloween!
Animal rescue
Rescue animals from trash and man-made environmental hazards, e.g., being tangled in plastic bags Sponsored by #byetobags
2016 Games
2015 Games
2014 Games
#stlscatterjam2014 Tweets
Streaming Instructions

subset: commoncrawl


text:
If an item you ordered from TextbookRush does not meet your expectations due to an error on our part, simply fill out a return request and then return it by mail within 30 days of ordering it for a full refund of item cost.
Learn more about our returns policy
Description: Depression, once a subfield of neurosis, has become the most diagnosed mental disorder in the world. Why and how has depression become such a topical illness and what does it tell us about changing ideas of the individual and society? Alain Ehrenberg investigates the history of depression and depressive symptoms across twentieth-century psychiatry, showing that identifying depression is far more difficult than a simple diagnostic distinction between normal and pathological sadness - the one constant in the history of depression is its changing definition. Drawing on the accumulated knowledge of a lifetime devoted to the study of the individual in modern democratic society, Ehrenberg shows that the phenomenon of modern depression is not a construction of the pharmaceutical industry but a pathology arising from inadequacy in a social context where success is attributed to, and expected of, the autonomous individual. In so doing, he provides both a novel and convincing description of the illness that clarifies the intertwining relationship between its diagnostic history and changes in social norms and values. The first book to offer both a global sociological view of contemporary depression and a detailed description of psychiatric reasoning and its transformation - from the invention of electroshock therapy to mass consumption of Prozac - The Weariness of the Self offers a compelling exploration of depression as social fact.
Limited time offer:
Get the first one free! (?)
All the information you need in one place! Each Study Brief is a summary of one specific subject; facts, figures, and explanations to help you learn faster.
List price: $59.95Copyright year: 2010Publisher: McGill-Queen's University PressPublication date: 2/1/2010Binding: HardcoverPages: 304Size: 6.50" wide x 9.25" long x 1.50" tall Weight: 1.496Language: English
*A minimum purchase of $35 is required. Shipping is provided via FedEx SmartPost®
and FedEx Express Saver®. Average delivery time is 1 – 5 business days, but
is not guaranteed in that timeframe. Also allow 1 - 2 days for processing. Free shipping is eligible only in the continental United States and excludes
Hawaii, Alaska and Puerto Rico. FedEx service marks used by permission."Marketplace"
orders are not eligible for free or discounted shipping.
Learn more about the TextbookRush


text: To get an idea of what Tunisia is truly like, take a look through the videos in our gallery above. Get a taste of a land full of souks and spices, waiting to welcome you with open arms. Allow yourself to be inspired and charmed by this cultural African country and all that it has to offer to its visitors. Get an idea of what holidays to Tunisia are really like and imagine yourself soaking up the warm African sun on your dream Tunisia holiday.


text: Pauloa Patterns 1029 circa 1970s/80s. Misses' Dress Contents[show] Links to reviews/blog postsEdit Sources/VendorsEdit Sew Exciting Needleworks CloesCloset GalleryEdit WishlistEdit Retrieved from "http://vintagepatterns.wikia.com/wiki/Pauloa_1029?oldid=607041" Ad blocker interference detected! Wikia is a free-to-use site that makes money from advertising. We have a modified experience for viewers using ad blockers Wikia is not accessible if you've made further modifications. Remove the custom ad blocker rule(s) and the page will load as expected. Categories: Vintage Sewing Patterns Pauloa 1970s Muu Muus Contrast High Waist Dresses Scoop Neck Dolman Sleeves Braid Trim Band Trim Maxi Add category Cancel Save


text:
Your Store:
item(s) totaling $
See if this part fits a specific vehicle.
|This product doesnt fit any of your saved vehicles
|Check Fit for another vehicle
|Parts Pack(s):
REVIEW SNAPSHOT®by PowerReviews
Reviewed by 2 customers
Best Uses
Comments about Monroe Strut-Mate Strut Mounting Kit:
Solid build and design, which I was concerned about for the price. I got the right one for my application the first time. It comes with four new replacement nuts so you can trash those old rusted ones after taking them off. The bearing appears to be solid, we'll see how it fairs over time. Overall, comparable or better than stock.
Best Uses
Comments about Monroe Strut-Mate Strut Mounting Kit:
I replaced the original struts and figured I would replace the mounts also. The original still were good even being 12 years old. I did not even get 3 years out of these. What a joke. Who cares about the warrenty if you have to do the job over and over.
I will scrap this C_R_A_P and buy Mazda parts.
I rather pay 20 dollars more and get a part that will last.


text:
But did it not strike you all that there would be a vacuum in the middle order?
No, the middle order was packed with me, Anju and Chander.
Precisely! With you all being openers is it not a new role for you all to be playing the in middle order?
I was always assigned to go one drop with Chander two and then Anju. But at the fall of Smitha's wicket it was decided that Chander would go ahead of me.
So, eventually both the openers ended up in the middle order. Moreover, the act of having one opener and a pinch hitter is justifiable but what sense does it make to have two pinch hitters? Normally, if out of the two batsmen at the crease one is going great guns then it is advisable for the other to drop anchor and revolve around the other. Having two batsmen go for their strokes, one felt was asking for trouble?
Well, at that time it was the best decision we all could come up with. Yes, it was risky but all of us were very positive that it was going to pay off. Today, we can say it did not pay off and we should not have done that.
Yes, that's exactly what I intended to drive home when I said, Conducting an experiment of such a magnitude in the semis was a risk because you don't have a second chance to say we shouldn't have done that and this?
Yeah, it probably could be termed as an experiment but then given the experience of Purnima and Smitha we were confident it would pay off. Again I stress that it was probably the big occasion that got to us because even in our camps we had worked out the various combinations.
In fact Purnima went opening in quite a few of those practice matches. Even with our fielding we had done a lot of work in the camps. It's just that we had a bad game on the big day.
So in the final analysis, mentally you all caved in. Though you had all prepared well with sufficient practice, eventually lack of mental preparedness did you in. So given this revelation do you suppose in future you need somebody working on the mental aspect of the game also?
Yes, along with our technique and basics we need mental coaching and mental strengthening and professional at that.
Switching topics and coming to the domestic front, I haven't seen much of an improvement, at least in the past 10 years - in terms of the game being marketed and packaged? As a result we are still struggling to hold our basic tournaments on a regular basis. Do you see things changing or will women's cricket continue to be were it is?
No I feel women's cricket has come up, especially after this World Cup. This World Cup has helped women's cricket to a great extent in terms of publicity. Now with the Internet coming into the scene may be people are bring made aware of the sport.
Part II to follow


text:
We strongly believe two things: software should satisfy the needs of the people who will be using it the process of software development is rewarding and fun.
We strongly believe two things:
- software should satisfy the needs of the people who will be using it
- the process of software development is rewarding and fun.
Because we hold these values, our Applied Computing degree is rather special. We focus on software engineering and user centred design rather than mathematics. As a result, our students are successful, employable, employed and proud of what they do.
"Knowledge is great, but applying it is better!"
BSc (Hons) Applied Computing is a degree for people who are creative, problem-solvers, good team-players and who enjoy a challenge. It is about the satisfaction of software development, not about office applications.
Our course is modelled on good practice in industry, and we update it annually to safeguard its relevance to the real world. It is successful too - our students are nationally recognised for the quality of their project work.
You will have 24-hour access to our award winning Queen Mother Building. It has an unusual mixture of lab space and breakout areas, with a range of conventional and special equipment for you to use. You can use your own laptop, if you wish to; wireless access is available throughout the building.
Professional accreditation
- This programme is accredited by the British Computer Society, for the purposes of fully meeting the academic requirement for registration as a Chartered IT Professional, fully meeting the academic requirement for Incorporated Engineer, partially meeting the academic requirement for a Chartered Engineer (on behalf of the Engineering Council) and partially meeting the academic requirement for registration as a Chartered Scientist (on behalf of the Science Council).
Students can use a range of equipment such as servers, Macs, Arduino systems and programming kit for games consoles such as the Nintendo Wii and Sony Playstation.
Our graduates have been:
- 10 times prize-winners in the Scottish 'Young Software Engineer of the Year' Awards run by the industry body Scotland IS
- short listed in Computing magazine's 'Best Student Project of the Year' award, and a winner in 2008
- twice finalists in the 'Best IT Student' in the UK-wide Science, Engineering and Technology Student of the Year competition
Entry Requirements
The following are the minimum, up-to-date entry requirements.
|Courses starting 2017
|Level 1 Entry
|Advanced Entry to Level 2
|SQA Higher/Advanced Higher
|BBBC (minimum) - ABBB (typical) at Higher including two science subjects (computing science is recommended), plus mathematics (Standard Grade at 3 or National 5/Intermediate2 at C).
Please see Notes below for a list of suitable science subjects.
|BB at Advanced Higher including two science subjects, plus BB at Higher in different subjects, plus mathematics (Standard Grade at 3 or National 5/Intermediate2 at C) and completion of the University's Java Online module.
|GCE A-Level
|CCC (minimum) - BBB (typical) including two science subjects (computing science is recommended), plus GCSE mathematics at C.
Please see Notes below for a list of suitable science subjects.
|ABB including two science subjects, plus GCSE mathematics at C and completion of the University's Java Online module.
|Irish Leaving Certificate (ILC)
|ABBB at Higher Level including two science subjects (computing science is recommended), plus Standard Level mathematics at grade 4.
Please see Notes below for a list of suitable science subjects.
|Level 2 entry is not possible with this qualification
|International Baccalaureate (IB) Diploma
|30 points at Higher Level grades 5, 5, 5 to include two science subjects (computing science is recommended), plus Standard Level mathematics at grade 4.
Please see Notes below for a list of suitable science subjects.
A combination of IB Certificate plus other qualifications, such as A-Levels, Advanced Placement Tests or the International Baccalaureate Career-related Programme (IBCP), will also be considered.
|34 points at Higher Level grades 6, 6, 5 to include two science subjects, plus Standard Level mathematics at grade 4 and completion of the University's Java Online module.
|Graduate Entry
|A relevant BTEC Extended Diploma with DDM
|A relevant HND with Merits in appropriate Science modules
A relevant BTEC Extended Diploma with DDD, plus completion of the University's Java Online module.
|SQA Higher National (HNC/HND)
|A relevant HNC with grade B in the Graded Unit
|A relevant HNC with grade A in the Graded Unit and 120 SCQF credits or a relevant HND with grades BB in the Graded Units and completion of the University's Java Online module.
|Scottish Baccalaureate
|Pass with CC at Advanced Higher in 2 Sciences or Mathematics and a Science
|Pass with BB at Advanced Higher in 2 Sciences or Mathematics and a Science and completion of the University's Java Online module.
|SWAP Access
|Relevant science subject with ABB grades to include Mathematics at SCQF Level 6
|Level 2 entry is not possible with this qualification
|Advanced Diploma
|Grade B with ASL-A Levels in 2 Sciences/Mathematics and a Science at BB
|Grade B with ASL-A Levels in 2 Sciences/Mathematics and a Science at AB and completion of the University's Java Online module.
|Welsh Baccalaureate
|Pass with A-Levels in 2 Sciences/Mathematics and a Science at BB
|Pass with A-Levels in 2 Sciences/Mathematics and a Science at AB and completion of the University's Java Online module.
|European Baccalaureate
|70% overall with 7 in 2 Sciences/Mathematics and a Science
|75% overall with 7.5 in 2 Sciences/Mathematics and a Science, plus completion of the University's Java Online module.
|Other Qualifications
|Suitable science subjects include: information technology, mathematics, chemistry, biology, human biology, physics, psychology or computing science.
EU and International qualifications
English Language Requirement
For non EU students
|IELTS Overall
Equivalent grades from other test providers
English Language Programmes
We offer Pre-Sessional and Foundation Programme(s) throughout the year. These are designed to prepare you for university study in the UK when you have not yet met the language requirements for direct entry onto a degree programme.
Teaching Excellence Framework (TEF)
The University of Dundee has been given a Gold award – the highest possible rating – in the 2017 Teaching Excellence Framework (TEF).
Teaching & Assessment
How you will be taught
We know that the best way to learn how to design good software is to practise designing good software. You will learn to apply good software engineering principles, whatever the language or technology or platform: Java, C++, C#, Unity, ASP.NET, SQL, NoSQL OpenGL, UNIX and many more.
We also know how important it is to be at the leading edge of computing and so you will learn from research-active staff. Leading researchers teach from your first year through to your final year. Our smaller classes mean that we really get to know you, making for an informal and supportive community.
Industrial collaboration is part of our ethos too, so we regularly include guest experts from industry.
How you will be assessed
You will be assessed by a combination of practical coursework (20% - 60% of a module mark, typically) and end-of-semester examination.
Coursework is often very practical, e.g. writing computer programs, designing interfaces, writing reports, constructing web sites, testing software, implementing databases, analysing problems or presenting solutions to clients.
What you will study - Computing and Cognitive Science
Honours Degree
An honours degree normally takes four years, full time, you study levels 1-4, as described below.
Advanced Entry Honours Degree
It is possible to study for most of our honours degrees in three years if you have the required grades and subjects as listed in the Entry Requirements section. You study levels 2-4 below. There are definite advantages to considering this route as the time needed to study is reduced by one year which enables you to start working and earning earlier.
Degree without Honours
If you choose to study a degree without honours, you study for three years, levels 1-3 below.
Typical Degree Programme
Detailed module guides are available online
Level 1
You will cover the basics of programming, and start to think about how you can create programs for different purposes.
- AC11001 Introduction to software development
- AC11002 Web authoring
- AC12001 Introduction to Data Structures and Algorithms
- AC12003 Argumentation
- AC21010 Data visualisation
- AC22006 Physical computing
Level 2
You will expand upon your programming knowledge to include different languages. You will also learn about hardware and how your programs are implemented at this level.
- AC21007 Algorithms and Artificial Intelligence
- AC21008 Multi-paradigm programming
- AC21009 Computer Systems 2A
- AC22003 Information Technology Project
- AC22004 Object-oriented analysis and design
- AC22005 Computer Systems 2B
Level 3
You will sharpen your degree focus with specialist modules in key areas. At this stage you are given more control over what languages you use and how you approach different problems.
- AC31007 Agile Software Engineering
- AC31008 Networks and Data Communications
- AC31009 Games Programming
- AC32005 Human Computer Interaction
- AC32006 Database Systems
- AC32007 Secure Internet Programming
Between Level 3 and Level 4, you can take a Work Placement which contributes to your degree. (see AC41010 Work Placement).
Level 4
- AC41001 Individual Project
- AC41004 Industrial Team Project
- Two modules from the following:
- AC41001 Graphics
- AC41002 Computer Vision
AC41007 Technology Innovation Management
- AC41001 Big Data Analysis
- AC41012 User Experience
- AC42001 Research Frontiers. You will have the choice of four sub-modules from options. These options change regularly because they are linked to our current research, but may include:
- Constraints Programming
- Teaching Computing
- Assistive Technology
- Argumentation
BSc (Hons) Applied Computing is accredited by the British Computer Society, the Chartered Institute for IT professionals in the UK and abroad.
Our students are highly employable:
- They develop the expertise that employers want from computing graduates - our Industrial Advisory Board includes experts from a range of industries including Amazon, Scottish Enterprise Tayside, NCR, Chevron and Microsoft.
- Many modules contain industrial case studies or projects where you can solve problems that our industrial partners are facing at that time.
- They can gain work placement experience for degree credit - if you want, take a work placement in the summer vacation between Level 3 and Level 4 - it gives you valuable 'real world' work experience and a good insight into working in the computing industry. Recent work placements have been with Microsoft, NHS, Avian, Yahoo!, NCR and Cohort Studios.
- They are prepared for a wide range of good career prospects in computing - the UK faces a massive shortage of graduates qualified to fill the 120,000 new jobs in computing and IT every year.
Boris Borisov, BSc Applied Computing, Intelligent Point of Sale Ltd
"I work for Intelligent Point of Sale Ltd, who develop point of sale solutions for iPads. I am in charge of all the server side aspects of developing our software. My studies prepared me really well for the job I am doing now. The course allowed me to develop specific knowledge in areas that have become really handy. I'm really happy that I chose Dundee and I'd recommend it to anyone who is considering studying at the University."
Lyuben Todorov, BSc Applied Computing, Big Data Developer
"I am a big data developer. I work with Cassandra and other leading-edge technologies. My day-to-day involves working with extremely large systems. There was a very specific course on big data which I studied in my final year. The course gave me a great insight into what industry is looking for and what the next hot technology will be. They just knew the way software development would turn. They saw a pattern which pointed towards big data. Everyone uses big data now."
Fees & Funding
The fees you pay will depend on your fee status. Your fee status is determined by us using the information you provide on your application.
Find out more about fee status
Fees for students starting 2017/18
|Fee category
|Fees for students starting 2017/18
|Scottish and EU students
|£1,820 per year of study (for Sept 2016 entry). Fees for September 2017 will be confirmed by the Scottish Government in early 2017.
|Rest of UK students
|£9,250 per year, for a maximum of 3 years, even if you are studying a four year degree. See our scholarships for rest of UK applicants.
|Overseas students (non-EU)
|£17,950 per year of study. See our scholarships for international applicants.
Scottish and EU students can apply to the Students Award Agency for Scotland (SAAS) to have tuition fees paid by the Scottish Government.
Rest of the UK students can apply for financial assistance, including a loan to cover the full cost of the tuition fees, from the Student Loans Company.
Tuition fees for Overseas (non-EU) students are guaranteed for the length of your course. This means that the tuition fee you pay in your first year (shown above) is the same fee you will pay for each year of your course. We guarantee that this will not increase while you are studying with us. The only exceptions to this are our MBChB Medicine, BSc Medical Sciences and BDS Dentistry degrees which charge a different tuition for the clinical years.
Your Application
Unistats data set - formerly the Key Information Set (KIS)
|UCAS Code
|Unistats Data
|Apply Now
|Applied Computing BSc (Hons)


text:
Colombian Authorities Capture Drug-Smuggling Submarine [VIDEO]
Acting on tips from informants, soldiers in Colombia have seized a 99-foot fully submersible submarine that was intended to be used for drug smuggling.
Acting on tips from informants, soldiers in Colombia have seized a 99-foot fully submersible submarine that was intended to be used for drug smuggling.
An Associated Press Live Event:
Wild cheers erupted from tens of thousands of demonstrators in Cairo's Tahrir Square after word spread that Egyptian President Hosni Mubarak has resigned. Demonstrators chanted "Egypt is free!" upon hearing the news.
According to NBC News, Egypt's President Hosni Mubarak will be stepping down tonight after weeks of relentless protests and violence in Cairo.
East Texas got snow and Australia got....a cyclone.
Check out some amazing shots of the aftermath of the worst cyclone in Australia's history, which hit Queensland yesterday...
Crowds boo and yell as the Egyptian President announces that he will not run for a term in September, but will continue to reign until then.
Due to the relentless uproar happening in Cairo, Secretary of State Hillary Rodham Clinton is convening an unprecedented mass meeting of U.S. ambassadors.
Hundreds of American citizens are doing everything they can to get out of Egypt any way they can today.
The first of two charter planes carrying U.S. citizens out of chaotic Egypt landed Monday in Cyprus, the beginning of what could be a lengthy evacuation effort amid escalating unrest across the country.


text:
Even though fights in hockey are almost as common as goals, it's not an everyday that the game's biggest superstars get into a brawl. But it happened on Thursday night when Pittsburgh Penguins captain Sidney Crosby got tangled up with Columbus Blue Jackets center Brandon Dubinsky, and the two got into a fistfight.
This is Crosby's 10th season in the NHL, and as per hockeyfights.com, he has only ever been involved in six fights. So what led to this usually level-headed fella to lose his mind? Well, Dubinsky is one irritating defender and is often assigned the job of marking Crosby. The two had problems even when Dubinsky used to play for the New York Rangers.
Hence, when Dubinsky went to check No. 87, he took exception and a punch-up ensued. It wasn't a grueling, bloody fight by any means. Actually, the two jostled more than trading blows. However, Crosby did land at least one clean shot to Dubinsky's face.
Check out the fight video above.
Also Check: Hockey Noob Takes On The Biggest Dude, Gets KO'd With Single Punch


text:
Thomas AndreOrillia, CA
Worked on my own skits and characters for 2 years officially
I have had month long immersion training at the second city in Chicago.
English (North American), English
North American
Child, Middle Aged, Senior, Teen, Young Adult
Special Skills
Audiobooks, Business, Cartoons, Documentaries, Educational, Internet, Jingles, Movie Trailers, Music, Podcasting, Radio, Telephone, Television, Videogames
Worked on my own skits and characters for 2 years officially
I have had month long immersion training at the second city in Chicago.
Second city - Writing and improve #1- #4 ( 8 week long courses
Computer & Software
MacBook Pro
Delivery Methods
Electronic delivery or otherwise
Payment Terms
Hire Thomas as a voice actor. Payment is made through Voices.com SurePay, an escrow service that guarantees your work is done to your satisfaction. Send payment securely by Visa, Mastercard or PayPal through Voices.com then download your files from the website.
Watch a video to see how to make a payment
Next Steps
To contact Thomas Andre about your project, request a quote today. We'll walk you through the process step-by-step. It's fast and easy.
This talent has not uploaded any demos yet.
Title of Your New Demo 7777 Listens
Hire Thomas Andre as a voice actor. Working with Thomas Andre is fast and easy. We'll walk you through the process step-by-step.
Request a quote for your project today.