Muutke küpsiste eelistusi

E-raamat: System Architecture: An Ordinary Engineering Discipline

, , ,
  • Formaat: PDF+DRM
  • Ilmumisaeg: 04-Oct-2016
  • Kirjastus: Springer International Publishing AG
  • Keel: eng
  • ISBN-13: 9783319430652
Teised raamatud teemal:
  • Formaat - PDF+DRM
  • Hind: 55,56 €*
  • * hind on lõplik, st. muud allahindlused enam ei rakendu
  • Lisa ostukorvi
  • Lisa soovinimekirja
  • See e-raamat on mõeldud ainult isiklikuks kasutamiseks. E-raamatuid ei saa tagastada.
System Architecture: An Ordinary Engineering DisciplineSuurem pilt
  • Formaat: PDF+DRM
  • Ilmumisaeg: 04-Oct-2016
  • Kirjastus: Springer International Publishing AG
  • Keel: eng
  • ISBN-13: 9783319430652
Teised raamatud teemal:

DRM piirangud

  • Kopeerimine (copy/paste):

    ei ole lubatud

  • Printimine:

    ei ole lubatud

  • Kasutamine:

    Digitaalõiguste kaitse (DRM)
    Kirjastus on väljastanud selle e-raamatu krüpteeritud kujul, mis tähendab, et selle lugemiseks peate installeerima spetsiaalse tarkvara. Samuti peate looma endale  Adobe ID Rohkem infot siin. E-raamatut saab lugeda 1 kasutaja ning alla laadida kuni 6'de seadmesse (kõik autoriseeritud sama Adobe ID-ga).

    Vajalik tarkvara
    Mobiilsetes seadmetes (telefon või tahvelarvuti) lugemiseks peate installeerima selle tasuta rakenduse: PocketBook Reader (iOS / Android)

    PC või Mac seadmes lugemiseks peate installima Adobe Digital Editionsi (Seeon tasuta rakendus spetsiaalselt e-raamatute lugemiseks. Seda ei tohi segamini ajada Adober Reader'iga, mis tõenäoliselt on juba teie arvutisse installeeritud )

    Seda e-raamatut ei saa lugeda Amazon Kindle's. 

The pillars of the bridge on the cover of this book date from the Roman Empire and they are in daily use today, an example of conventional engineering at its best. Modern commodity operating systems are examples of current system programming at its best, with bugs discovered and fixed on a weekly or monthly basis. This book addresses the question of whether it is possible to construct computer systems that are as stable as Roman designs.The authors successively introduce and explain specifications, constructions and correctness proofs of a simple MIPS processor; a simple compiler for a C dialect; an extension of the compiler handling C with inline assembly, interrupts and devices; and the virtualization layer of a small operating system kernel. A theme of the book is presenting system architecture design as a formal discipline, and in keeping with this the authors rely on mathematics for conciseness and precision of arguments to an extent common in other engineering fields.This

textbook is based on the authors" teaching and practical experience, and it is appropriate for undergraduate students of electronics engineering and computer science. All chapters are supported with exercises and examples.

Introduction.- Understanding Decimal Addition.- Basic Mathematical Concepts.- Number Formats and Boolean Algebra.- Hardware.- Five Designs of RAM.- Arithmetic Circuits.- A Basic Sequential MIPS Machine.- Some Assembler Programs.- Context-Free Grammars.- The Language C0.- A C0-Compiler.- Compiler Consistency Revisited.- Operating System Support.- A Generic Operating System Kernel.
1 Introduction
1(6)
2 Understanding Decimal Addition
7(8)
2.1 Experience Versus Understanding
7(1)
2.2 The Natural Numbers
8(5)
2.2.1 2 + 1 = 3 is a Definition
9(1)
2.2.2 1 + 2 = 3 is a Theorem
9(2)
2.2.3 9 + 1 = 10 is a Brilliant Theorem
11(2)
2.3 Final Remarks
13(1)
2.4 Exercises
14(1)
3 Basic Mathematical Concepts
15(18)
3.1 Basics
16(5)
3.1.1 Implicit Quantification
16(1)
3.1.2 Numbers and Sets
17(1)
3.1.3 Sequences, Their Indexing and Overloading
18(2)
3.1.4 Bytes, Logical Connectives, and Vector Notation
20(1)
3.2 Modulo Computation
21(3)
3.3 Sums
24(1)
3.3.1 Geometric Sums
24(1)
3.3.2 Arithmetic Sums
25(1)
3.4 Graphs
25(4)
3.4.1 Directed Graphs
25(2)
3.4.2 Directed Acyclic Graphs and the Depth of Nodes
27(1)
3.4.3 Rooted Trees
28(1)
3.5 Final Remarks
29(1)
3.6 Exercises
30(3)
4 Number Formats and Boolean Algebra
33(18)
4.1 Binary Numbers
33(4)
4.2 Two's Complement Numbers
37(2)
4.3 Boolean Algebra
39(8)
4.3.1 Useful Identities
42(2)
4.3.2 Solving Equations
44(1)
4.3.3 Disjunctive Normal Form
45(2)
4.4 Final Remarks
47(1)
4.5 Exercises
48(3)
5 Hardware
51(20)
5.1 Gates and Circuits
51(5)
5.2 Some Basic Circuits
56(4)
5.3 Clocked Circuits
60(6)
5.4 Registers
66(1)
5.5 Final Remarks
66(1)
5.6 Exercises
67(4)
6 Five Designs of RAM
71(10)
6.1 Basic Random Access Memory
71(2)
6.2 Read-Only Memory (ROM)
73(1)
6.3 Combining RAM and ROM
73(2)
6.4 Three-Port RAM for General-Purpose Registers
75(2)
6.5 SPR-RAM
77(2)
6.6 Final Remarks
79(1)
6.7 Exercises
79(2)
7 Arithmetic Circuits
81(28)
7.1 Adder and Incrementer
81(8)
7.1.1 Carry Chain Adder and Incrementer
82(1)
7.1.2 Conditional-Sum Adders
83(3)
7.1.3 Parallel Prefix Circuits
86(2)
7.1.4 Carry-Look-Ahead Adders
88(1)
7.2 Arithmetic Unit
89(5)
7.3 Arithmetic Logic Unit (ALU)
94(2)
7.4 Shifter
96(2)
7.5 Branch Condition Evaluation Unit
98(2)
7.6 Final Remarks
100(1)
7.7 Exercises
101(8)
8 A Basic Sequential MIPS Machine
109(36)
8.1 Tables
110(2)
8.1.1 I-type
110(1)
8.1.2 R-type
111(1)
8.1.3 J-type
111(1)
8.2 MIPS ISA
112(11)
8.2.1 Configuration and Instruction Fields
112(2)
8.2.2 Instruction Decoding
114(1)
8.2.3 ALU Operations
115(3)
8.2.4 Shift
118(1)
8.2.5 Branch and Jump
118(2)
8.2.6 Loads and Stores
120(2)
8.2.7 ISA Summary
122(1)
8.3 A Sequential Processor Design
123(17)
8.3.1 Hardware Configuration
123(2)
8.3.2 Fetch and Execute Cycles
125(1)
8.3.3 Reset
125(1)
8.3.4 Instruction Fetch
126(2)
8.3.5 Proof Goals for the Execute Stage
128(1)
8.3.6 Instruction Decoder
128(4)
8.3.7 Reading from General-Purpose Registers
132(1)
8.3.8 Next PC Environment
133(2)
8.3.9 ALU Environment
135(1)
8.3.10 Shifter Environment
136(1)
8.3.11 Jump and Link
137(1)
8.3.12 Collecting Results
137(1)
8.3.13 Effective Address
138(1)
8.3.14 Memory Environment
138(2)
8.3.15 Writing to the General-Purpose Register File
140(1)
8.4 Final Remarks
140(1)
8.5 Exercises
141(4)
9 Some Assembler Programs
145(14)
9.1 Simple MIPS Programs
146(1)
9.2 Software Multiplication
147(2)
9.3 Software Division
149(7)
9.3.1 School Method for Non-negative Integer Division
149(1)
9.3.2 `Small' Unsigned Integer Division
150(3)
9.3.3 Unsigned Integer Division
153(2)
9.3.4 Integer Division
155(1)
9.4 Final Remarks
156(1)
9.5 Exercises
156(3)
10 Context-Free Grammars
159(20)
10.1 Introduction to Context-Free Grammars
160(8)
10.1.1 Syntax of Context-Free Grammars
160(1)
10.1.2 Quick and Dirty Introduction to Derivation Trees
161(2)
10.1.3 Tree Regions
163(2)
10.1.4 Clean Definition of Derivation Trees
165(2)
10.1.5 Composition and Decomposition of Derivation Trees
167(1)
10.1.6 Generated Languages
168(1)
10.2 Grammars for Expressions
168(7)
10.2.1 Syntax of Boolean Expressions
168(2)
10.2.2 Grammar for Arithmetic Expressions with Priorities
170(1)
10.2.3 Proof of Lemma 66
171(4)
10.2.4 Distinguishing Unary and Binary Minus
175(1)
10.3 Final Remarks
175(1)
10.4 Exercises
176(3)
11 The Language C0
179(74)
11.1 Grammar of C0
180(10)
11.1.1 Names and Constants
180(2)
11.1.2 Identifiers
182(1)
11.1.3 Arithmetic and Boolean Expressions
183(1)
11.1.4 Statements
183(1)
11.1.5 Programs
184(1)
11.1.6 Type and Variable Declarations
184(1)
11.1.7 Function Declarations
185(1)
11.1.8 Representing and Processing Derivation Trees in C0
186(3)
11.1.9 Sequence Elements and Flattened Sequences in the C0 Grammar
189(1)
11.2 Declarations
190(9)
11.2.1 Type Tables
190(3)
11.2.2 Global Variables
193(1)
11.2.3 Function Tables
194(2)
11.2.4 Variables and Subvariables of all C0 Configurations
196(1)
11.2.5 Range of Types and Default Values
197(2)
11.3 CO Configurations
199(11)
11.3.1 Variables, Subvariables, and Their Type in CO Configurations c
199(3)
11.3.2 Value of Variables, Type Correctness, and Invariants
202(2)
11.3.3 Expressions and Statements in Function Bodies
204(3)
11.3.4 Program Rest
207(2)
11.3.5 Result Destination Stack
209(1)
11.3.6 Initial Configuration
209(1)
11.4 Expression Evaluation
210(12)
11.4.1 Type, Right Value, and Left Value of Expressions
212(2)
11.4.2 Constants
214(1)
11.4.3 Variable Binding
215(2)
11.4.4 Pointer Dereferencing
217(1)
11.4.5 Struct Components
217(1)
11.4.6 Array Elements
218(1)
11.4.7 `Address of'
219(1)
11.4.8 Unary Operators
219(2)
11.4.9 Binary Operators
221(1)
11.5 Statement Execution
222(10)
11.5.1 Assignment
223(1)
11.5.2 Conditional Statement
224(1)
11.5.3 While Loop
224(1)
11.5.4 `New' Statement
225(2)
11.5.5 Function Call
227(3)
11.5.6 Return
230(2)
11.6 Proving the Correctness of C0 Programs
232(14)
11.6.1 Assignment and Conditional Statement
232(2)
11.6.2 Computer Arithmetic
234(1)
11.6.3 While Loop
234(2)
11.6.4 Linked Lists
236(6)
11.6.5 Recursion
242(4)
11.7 Final Remarks
246(2)
11.8 Exercises
248(5)
12 A C0-Compiler
253(80)
12.1 Compiler Consistency
254(21)
12.1.1 Memory Map
254(2)
12.1.2 Size of Types, Displacement, and Base Address
256(4)
12.1.3 Consistency for Data, Pointers, and the Result Destination Stack
260(2)
12.1.4 Consistency for the Code
262(2)
12.1.5 Consistency for the Program Rest
264(6)
12.1.6 Relating the Derivation Tree and the Program Rest
270(5)
12.2 Translation of Expressions
275(27)
12.2.1 Sethi-Ullman Algorithm
275(5)
12.2.2 The R-label
280(6)
12.2.3 Composable MIPS Programs
286(2)
12.2.4 Correctness of Code for Expressions
288(2)
12.2.5 Constants
290(1)
12.2.6 Variable Names
291(2)
12.2.7 Struct Components
293(1)
12.2.8 Array Elements
294(1)
12.2.9 Dereferencing Pointers
295(1)
12.2.10 `Address of'
296(1)
12.2.11 Unary Operators
297(1)
12.2.12 Binary Arithmetic Operators
298(2)
12.2.13 Comparison
300(1)
12.2.14 Translating Several Expressions and Maintaining the Results
301(1)
12.3 Translation of Statements
302(14)
12.3.1 Assignment
303(1)
12.3.2 New Statement
304(1)
12.3.3 While Loop
305(2)
12.3.4 If-Then-Else
307(1)
12.3.5 If-Then
308(1)
12.3.6 Function Call
308(5)
12.3.7 Return
313(2)
12.3.8 Summary of Intermediate Results
315(1)
12.4 Translation of Programs
316(6)
12.4.1 Statement Sequences
316(1)
12.4.2 Function Bodies
317(1)
12.4.3 Function Declaration Sequences
318(1)
12.4.4 Programs
318(2)
12.4.5 Jumping Out of Loops and Conditional Statements
320(2)
12.5 Compiler Correctness Revisited
322(3)
12.5.1 Christopher Lee and the Truth About Life After Death
322(1)
12.5.2 Consistency Points
323(1)
12.5.3 Compiler Correctness for Optimizing Compilers
324(1)
12.6 Final Remarks
325(1)
12.7 Exercises
326(7)
13 Compiler Consistency Revisited
333(42)
13.1 Reconstructing a Well-Formed CO Configuration
334(21)
13.1.1 Associating Code Addresses with Statements and Functions
335(2)
13.1.2 Reconstructing Everything Except Heap and Pointers
337(3)
13.1.3 Reachable Subvariables
340(2)
13.1.4 Implementation Subvariables
342(5)
13.1.5 Heap Reconstruction Is not Unique
347(1)
13.1.6 Heap Isomorphisms and Equivalence of CO Configurations
348(3)
13.1.7 Computations Starting in Equivalent Configurations
351(4)
13.2 Garbage Collection
355(10)
13.2.1 Pointer Chasing
356(4)
13.2.2 Garbage-Collected Equivalent Configurations
360(2)
13.2.3 Construction of a Garbage-Collected MIPS Configuration
362(3)
13.3 C0 + Assembly
365(7)
13.3.1 Syntax
365(1)
13.3.2 Compilation
366(1)
13.3.3 Semantics and Compiler Correctness
367(5)
13.4 Final Remarks
372(1)
13.5 Exercises
373(2)
14 Operating System Support
375(54)
14.1 Interrupts
376(8)
14.1.1 Types of Interrupts
376(1)
14.1.2 Special Purpose Registers and New Instructions
376(2)
14.1.3 MIPS ISA with Interrupts
378(3)
14.1.4 Specification of Most Internal Interrupt Event Signals
381(1)
14.1.5 Hardware
381(3)
14.1.6 Hardware Correctness
384(1)
14.2 Address Translation
384(7)
14.2.1 Specification
385(3)
14.2.2 Hardware
388(3)
14.3 Disks
391(30)
14.3.1 Hardware Model of a Disk
392(3)
14.3.2 Accessing a Device with Memory-Mapped I/O
395(2)
14.3.3 Nondeterminism Revisited
397(3)
14.3.4 Nondeterministic ISA for Processor + Disk
400(4)
14.3.5 Hardware Correctness
404(2)
14.3.6 Order Reduction
406(4)
14.3.7 Disk Liveness in Reordered Computations
410(4)
14.3.8 C0 + Assembly + Disk + Interrupts
414(3)
14.3.9 Hard Disk Driver
417(4)
14.4 Final Remarks
421(3)
14.5 Exercises
424(5)
15 A Generic Operating System Kernel
429(74)
15.1 Physical and Virtual Machines
431(3)
15.1.1 Physical Machines
431(1)
15.1.2 Virtual Machines
431(3)
15.2 Communicating Virtual Machines
434(4)
15.2.1 Configurations
434(1)
15.2.2 Semantics
435(3)
15.3 Concrete Kernel
438(14)
15.3.1 Data Structures
439(2)
15.3.2 Virtual Address Translation via C Data Structures
441(1)
15.3.3 Simulation Relation for Virtual Machines
442(2)
15.3.4 Encoding an Abstract Kernel by a Concrete Kernel
444(2)
15.3.5 Simulation Relation for the Abstract Kernel of CVM
446(3)
15.3.6 Technical Invariants
449(1)
15.3.7 Formulating the Correctness Theorem
450(2)
15.4 The runvm Primitive
452(9)
15.4.1 Overview of the runvm Primitive
453(1)
15.4.2 Program Annotations
454(1)
15.4.3 Maintaining k-consis
455(3)
15.4.4 Maintaining consis
458(1)
15.4.5 Maintaining inv-vm
459(2)
15.5 Simulation of CVM Steps
461(17)
15.5.1 Scratch Memory
461(2)
15.5.2 C0 Step of the Kernel
463(1)
15.5.3 IS A Step of a User Without Interrupt
464(2)
15.5.4 Restoring a User Process
466(4)
15.5.5 Testing for Reset
470(2)
15.5.6 Boot Loader and Initialization
472(2)
15.5.7 Process Save
474(4)
15.6 Page Fault Handling
478(12)
15.6.1 Testing for ipf Page Fault
478(3)
15.6.2 Auxiliary Data Structures
481(4)
15.6.3 Swapping a Page Out
485(2)
15.6.4 Swapping a Page In
487(3)
15.6.5 Liveness
490(1)
15.7 Other CVM Primitives and Dispatching
490(9)
15.7.1 Accessing Registers of User Processes
491(1)
15.7.2 Accessing User Pages
491(1)
15.7.3 Free and Alloc
492(5)
15.7.4 Application Binary Interface and Dispatcher for the Abstract Kernel
497(2)
15.8 Final Remarks
499(1)
15.9 Exercises
500(3)
References 503(4)
Index 507
Prof. Dr. Wolfgang J. Paul received his Ph.D. in 1973 from Saarland University. He did a postdoc in Cornell, and worked as a professor of mathematics in Bielefeld and in a research role with IBM in San Jose. He was appointed a professor in Saarbrücken in 1986, where he is now the Head of the Institute for Computer Architecture and Parallel Computing. He shared the Leibniz Prize in 1987 with Günter Hotz and Kurt Mehlhorn. He was the scientific director of the Verisoft project. His research interests include hardware design, computer architecture, and the formal verification of processors and microkernels.



Dr. Christoph Baumann received his Ph.D. in 2014 from Saarland University. As a staff member of the Institute for Computer Architecture and Parallel Computing he worked on the avionics component of the Verisoft XT project. Currently he is doing a postdoc at the KTH Royal Institute of Technology in Stockholm, working in the PROSPER and HASPOC projects on provably secure execution platforms for embedded systems. His research interests include the formal specification of modern processors, the formal verification of real-world operating systems, and information flow security.

Petro Lutsyk, M.Sc., is a scientific staff member of the Institute for Computer Architecture and Parallel Computing. His research interests include hardware design, hardware-assisted virtualization, and formal verification of hardware and low-level software.



Dr. Sabine Schmaltz received her Ph.D. in 2013 from Saarland University where she was a staff member of the Institute for Computer Architecture and Parallel Computing. She is currently creating a sewing community website while being a full-time caregiver for her son. Her research interests include operating systems, hypervisors, hardware architectures, compilers, formal verification, formal theories of systems, pervasive formal verification, and applied functional programming.
Lisainfo e-raamatute kohta Lisainfo e-raamatute kohta
Püsilink: https://www.kriso.ee/db/97833194306522e.html
Märksõnad: