Operating Systems ECS 251
Popular in Course
verified elite notetaker
Popular in Engineering Computer Science
This 6 page Class Notes was uploaded by Ashleigh Dare on Tuesday September 8, 2015. The Class Notes belongs to ECS 251 at University of California - Davis taught by Staff in Fall. Since its upload, it has received 65 views. For similar materials see /class/191716/ecs-251-university-of-california-davis in Engineering Computer Science at University of California - Davis.
Reviews for Operating Systems
Report this Material
What is Karma?
Karma is the currency of StudySoup.
You can buy or earn more Karma at anytime and redeem it for class notes, study guides, flashcards, and more!
Date Created: 09/08/15
Outline for January ll 2001 r N 9 gt V 0 gt1 ECS 251 7 Winter 2001 Page 1 Outline for January 11 2001 Greetings and felicitations a First part of project due Friday b Web page up and running Process models a Theorem If a system is mutually noninterfering it is determinate b Theorem Letfp be an interpretation of processp Let H be a system ofprocesses withp E H If for all such 7 domainp 0 and rangep 0 but fp unspeci ed is determinate for all fp then all processes in H are mutually noninterfering c Maximally parallel system determinate system for which the removal of any pair from the relation gt makes the two processes in the pair interfering processes Critical section problem a Mutual exclusion b Progress c Bounded wait Classical problems a Producerconsumer b Readerswriters rst readers priority second writers priority c Dining philosophers Basic language constructs a Semaphores b Sendreceive Evaluating higherlevel language constructs Modularity Constraints Expressive power Ease of use Portability Relationship with proram structure Process failures unanticipated faults exception handling Realtime systems rqowoposrrn Higherlevel language constructs Monitors Crowd monitors Invariant expressions CSP RPC ADATM Wop0579 Last modified at 1233 pm on Wednesday January 10 2001 Mutual NonInterference and Determinism ECS 251 7 Winter 2001 Page 2 Mutual NonInterference and Determinism Introduction A determinate system of processes is a set of process that always produces the same output given the same input A mutually noninterfering set of processes is a set of processes that do not interfere with the input or output of one another The question is to what degree are these the same concepts Formal De nitions and Notations A system of processes S gt is a set of processes H p1 pquot and a precedence relation gt HXH The gt relation is a partial ordering we de ne p gt p as true When 7 gt q process 7 must complete before pro cess q may begin Each process 7 E H has an associated set of input memory locations called domainp and an associated set of output memory locations rangeQJ Q An interpretatioan of p associates values with each set of memory loca tions The set of all inputs to S is abbreviated domainS and the set of all outputs from S is abbreviated rangeS Two systems of processes S gt and S 1T gt are equivalent if a H H b gt gtquot and c if S and S are given the same element of domainS then they output the same element of rangeS An execution sequence 06 is any string of process initiation and termination events satisfying the precedence con straints of the system ValIi 06 is the sequence of values written into memory locationAIi at the termination of processes in 06 The nal value stored inAIi after execution sequence 06 completes is represented by FatIi 06 A determinate system of processes is a system of processes S for which each element of domainS produces the same set rangeS regardless of the order or overlapping of the elements of S More formally a system S is deter minate if for any initial state and for all execution sequences 06 and 06 of S ValIi 06 ValIi 06 A mutually noninterfering system of processes is a system of processes S in which all pairs of processes meet the Bernstein conditions Processes p and q are noninterfering if either process is a predecessor of the other or the processes satisfy the Bernstein conditions The initiation of a process 7 is writtten and the termination of p is written 2 Relationship of Determinate Systems and Mutually Noninterfering Systems Theorem 1 If a system is mutually noninterfering it is determinate Theorem 2 Let S be a system with domainp and range speci ed range Q for all p E H and fp unspeci ed Then if S is determinate for all fp it is mutually noninterfering Proofs The following lemma is helpful Lemma Let S be a mutually noninterfering system Let p be a terminal process of S If 06 B57115 is an execution sequence of S then 06 B75172 is an execution sequence of S for which VM 06 ValIi 06 for all 139 Proof Asp is a terminal process in S it has no successors in S Hence 06 satis es the precedence constraints of S So 06 is an execution sequence We now consider two cases 1 IV E rangep Note 7 does not write memory locations not in rangep Consider any process 7 withIT in 5 As 7 and p are mutually noninterfering rangeQa n domainp Q So all such 7 nd the same values in domainQJ whether the execution sequence is 06 or 06 Thus ValIi 06 ValIi 06 IV E rangep LetITin 75 As 7 and p are mutually noninterfering domain A rangep Q So no 7 in 75 writes into an element of domainQJ Hence for allAIj E domainp Val1 B Val1 B75 By de nition for all IV E domainQJ B B75 As 7 has the same input for both 06 and 06 it writes the same value into 19 Last modified at 1233 pm on Wednesday January 10 2001 Mutual NonInterference and Determinism ECS 251 7 Winter 2001 Page 3 eachAIi E rangep in 06 and 06 Let v denote the value that p writes into IV in 06 Then ValIi 06 ValIi SI 1725 as no process 1 in 5 writes into an element of range VMs 31 70 V VMs 3 V VMs bY5 V V1V1st5I72 VMs 06 This proves the lemma I Proof of Theorem 1 We proceed by induction on the number k of processes in a system Basis k l The claim is trivially true Hypothesis For k l nil if a system of k processes is mutually noninterfering it is determinate Step Let S be an n process system of mutually noninterfering processes If S has exactly one execution sequence it is determinate So assume that S has two distinct execution sequences as p writes v into IV as no process 1 in ywrites into an element of rangep as no process 1 in ywrites into an element of rangep as p writes v into 1V1 oc and B Let p be a terminal process of S and form 06 and according to the lemma Then 06 Mfg ValIi 06 ValIi 06 for all 1 such that l S 1 S m B ValIi B ValIi for all 1 such that l S 1 S m Now form the nil process system S H E p gt where gt is formed by deleting from gt all pairs withp in them Clearly 06 and are execution sequences of S Further by the induction hypothesis ValIi 06 ValIi for all 1 such that l S 1 S m This means that the values in the elements of doma1np are the same in both 06 and in other words 06 for allAIj E dama1np As the inputs for p are the same in both execution sequences the outputs will also be the same It follows that p writes the same value v intoAIi E range in both 06 and Hence forAIi E rangeQa VM 0 Val1139 06 by the lemma VMigt 05 asMi E rangep Val1i by the induction hypothesis VMigt B asMi E rangep Val11gt B by the lemma and for M E rangeQa VM 0 VM 05 by the lemma VM 06 V p writes v into M Val1i V by the induction hypothesis VM B V p writes v into M Val11gt B by the lemma Either way ValIi 06 ValIi Hence S is determinate completing the induction step and the proof Proof of Theorem 2 We prove this theorem by contradiction Let S be a determinate system Let p p E H be inter fering processes Then there exist execution sequences 06 B17217 IL Y 06 31721727 Consider the Bernstein conditions Asp and p are interfering at least one of those conditions does not hold We examine them separately 1 LetAIi E rangep n rangep We choose the interpretatioan so that p writes the value 11 into 1 and we choose the interpretation fpx so that p writes the value v into 1 and 11 v But then VMigt 31 7217 117 3 VMzs 5 u V a d 1391 VM 3171152 VMs 3 V u This means S is not determinate contradicting hypothesis So range m rangep Q 19 LetAIi E domainQa n rangep As rangep Q take IV E rangep Choose the interpretation fpx so that 1 Last modified at 1233 pm on Wednesday January 10 2001 Outline for February 20 2001 r N 9 He Gre a Wri a b c Cac a b c d ECS 251 7 Winter 2001 Page 1 Outline for February 20 2001 etings and felicitations Tuesday Feb 20 3430 Friday Feb 23 110230 go to 1101 Hart Hall to view ting Policy Writethrough client writes to le server immediately updates le written Delayed write at server client writes to le server may hold before updating le39 idea is that data may not need to be written at all because client may delete it39 problem is crashes loose that data Delayed write at client writes sit at client until le is closed then are ushed to server Idea is that les are open for a very short time so this cuts burden on servers he consistency serverinitiated servers inform cache managers when data no longer valid clientinitiated client cache managers check validity of data before returning it to callers disallow caching when concurrentwrite sharing le open at multiple clients and at least one for writing either server tracks who has le open and how or lock it problem sequentialwrite sharing recently updated le by one client is opened for writing by a second cli ent Second may have outdated blocks in cache cache timestamps and compare with real timestamps rst client may not have ushed cached changes yet server requires clients to ush cache when another client opens le Availability via replication a 0 Replicate les i Can do only those that must be highly available ii Some attribute data eg protection rights stored with each replica iii May not reside on same server as containing directory Replicate volumes le systems i Easier to manage e g protection rights associated with volume ii Need to replicate volume if any le on it requires high availability Replicate legroups primary pack replica called a pack i Contains subset of les in primary pack Management consistency among replicas i Weighted voting scheme ii Agent processes Locus current storage site enforces the global synchronization policy Example NFS a 7 0 P Architecture built on RFC and using a virtual le interface a la UNIX modes Naming all workstations are conceptually clients and servers in practise have a few systems designated as le servers BFS downstairs discuss le handles it s stateless Lack of State simpli es crash recovery Handle contains all the info identifying the le and client kernel tracks le offsets etc If client hears nothing just resend i Server crashes just restart ii Messages bigger than stateful server would require but would also require restoring lots of info Caching client caches i File blocks on demand usually 8Kb blocks as is timestamp of last mod on server Timeout after some period of time then must revalidate ii Directory name lookups ushed when lookup fails andor new vnode info obtained iii File attributes90 of all NFS requests to server39 discarded after 3 sec les 30 sec directories Example Sprite a b 0 Architecture uses a virtual le interface built on multiple servers Naming global tree hierarchy39 each subtree is a domain and multiple domains may reside on one server39 pre x table maps le pre xes to servers each entry has full name of mount point server name and domain nam e39 to locate refer to pre x table and nd longest matching pre x then go there nif no entry broadcast for it39 server sends a le token for the le and this used to reference le Remote links return contained le names and client iterates Caching in main memory Last modified at 637 am on Tuesday February 27 2001 Outline for February 20 2001 gt1 00 0 ECS 251 7 Winter 2001 Page 2 File blocks addressed by le token and block number Query is to cache then local if there or remote if remote to cache then to le Delayed writing policy every 5 sec cached blocks not modi ed in last 30 sec are written back to server iii Replacement policy LRU Consistency serverinitiated approach39 les open for both reading and writing are not cached and when opened for such cached blocks are written back before open nished Example Coda descendant of AF S a Architecture highly scalable so clients take much of load through caching39 local client s disk treated entirely as a cache and clients can operate when disconnected b Naming uses volumes each le directory has a 92bit File 1D 32 bit volume number 32 bit vnode number 32 bit unique identi er Replication preserves Fle Servers have volume location databases name compo nents mapped to Fle and this info cached at client c Caching on volume creation number and location of volume replicas is set called a volume replication database39 set of servers called a volume storage group39 set of servers accessible to a client for every cached volume is called accesible volume storage group and is kept track of by client cache manager called Venus i On demand caching les cached in their entirety on client Obtained from a preferred server one of the AVSG if contacted one is not newest copy because some other member has a newer one that server becomes preferred server and previous preferred server noti ed it has stale data Callbacks set at preferred server agreement to notify client if le becomes stale39 then client invalidates cached le may get new copy On modi cation le sent back to all members of AVSG in parallel via hardware multicast E 1 Security a Goals con dentiality integrity availability b Basic Outline Foundations Policies Mechanisms Assurance Human and Operational Issues c Relationship of policy and mechanism and assurance d Foundations ACM model HRU result e Policies BLP con dentiality ClarkWilson integrity Chinese Wall both f Mechanism cryptography Cryptography basics cryptosystems attacks codes vs ciphers superencryption substitution ciphers Caesar cipher Vigenere cipher transposition ciphers railfence cipher product cipher DES public key crypto RSA DH cryptographic checksums key management Kerberos PKI digital signatures authentication Examples PEM PGP IPSec lt m r39 qowoposr Last modified at 637 am on Tuesday February 27 2001 Static Voting Protocol ECS 251 7 Winter 2001 Page 3 Static Voting Protocol Introduction This is the weighted voting protocol used to ensure mutual consistency among replicas The rules allow multiple readers and no writers or one writer and no readers Notation n sites S site L corresponding lock manager usually a process on the same site when L grants a LOCKiREQU39EST for a le it locks the le locally N version number of replica at site S V number ofvotes assigned to replica at site S r read quorum a read is allowed if r read votes are accumulated w write quorum a write is allowed if w write votes are accumulated v votes total Voting Algorithm In what follows we require that r w gt v and 2w gt v l S issues a LOCKiREQUEST to L 2 When LOCKiREQUEST granted S sends a VOTEiREQUEST message to all other processes 3 When receives a VOTEiREQUEST message a issues a LOCKiREQUEST to Lj b If LOCKiREQUEST granted returns and to S 4 S waits for some timeout period then determines if it has a quorum LetP be the set of sites from which replies have beenreceived and letQ SE P le max Nkl kE P a For a read request if V 25 E P VJ 2 r then S has a read quorum b For a write request if Vw 25 E Q VJ 2 w then S has a write quorum 5 If S does not obtain the desired quorum it issues a RELEASEiLOCK to L and all L J from which it has received votes that is all L with s E P 6 If S obtains a lock it checks that its local copy is current and if not obtains a current copy 7 If S requested a read a The local copy is read b S issues a RELEASEiLOCK to L and all L from which it has received votes that is all L with s E P 8 If S requested a write a The local copy is written b S updates N c S sends all the updates and N to all sites in Q d S issues a RELEASEiLOCK to L and all L from which it has received votes that is all L with s E P 9 If S receives an update it performs the update on its local copy 10 lfLi receives a RELEASEiLOCK it releases the local lock Guarantees None of the obsolete copies are updated due to a write quorum see 6 There is a subset of replicas that are current and whose votes total to w see 7 There is a nonnull intersection between every read quorum and every write quorum from the relationship Last modified at 637 am on Tuesday February 27 2001
Are you sure you want to buy this material for
You're already Subscribed!
Looks like you've already subscribed to StudySoup, you won't need to purchase another subscription to get this material. To access this material simply click 'View Full Document'