A Pipelined Multi-core MIPS Machine (Record no. 97172)

000 -LEADER
fixed length control field 08114nam a22006495i 4500
001 - CONTROL NUMBER
control field 978-3-319-13906-7
003 - CONTROL NUMBER IDENTIFIER
control field DE-He213
005 - DATE AND TIME OF LATEST TRANSACTION
control field 20240730202753.0
007 - PHYSICAL DESCRIPTION FIXED FIELD--GENERAL INFORMATION
fixed length control field cr nn 008mamaa
008 - FIXED-LENGTH DATA ELEMENTS--GENERAL INFORMATION
fixed length control field 141124s2014 sz | s |||| 0|eng d
020 ## - INTERNATIONAL STANDARD BOOK NUMBER
International Standard Book Number 9783319139067
-- 978-3-319-13906-7
024 7# - OTHER STANDARD IDENTIFIER
Standard number or code 10.1007/978-3-319-13906-7
Source of number or code doi
050 #4 - LIBRARY OF CONGRESS CALL NUMBER
Classification number QA76.9.A43
072 #7 - SUBJECT CATEGORY CODE
Subject category code UMB
Source bicssc
072 #7 - SUBJECT CATEGORY CODE
Subject category code COM051300
Source bisacsh
072 #7 - SUBJECT CATEGORY CODE
Subject category code UMB
Source thema
082 04 - DEWEY DECIMAL CLASSIFICATION NUMBER
Classification number 518.1
Edition number 23
100 1# - MAIN ENTRY--PERSONAL NAME
Personal name Kovalev, Mikhail.
Relator term author.
Relationship aut
-- http://id.loc.gov/vocabulary/relators/aut
9 (RLIN) 172944
245 12 - TITLE STATEMENT
Title A Pipelined Multi-core MIPS Machine
Medium [electronic resource] :
Remainder of title Hardware Implementation and Correctness Proof /
Statement of responsibility, etc. by Mikhail Kovalev, Silvia M. Müller, Wolfgang J. Paul.
250 ## - EDITION STATEMENT
Edition statement 1st ed. 2014.
264 #1 - PRODUCTION, PUBLICATION, DISTRIBUTION, MANUFACTURE, AND COPYRIGHT NOTICE
Place of production, publication, distribution, manufacture Cham :
Name of producer, publisher, distributor, manufacturer Springer International Publishing :
-- Imprint: Springer,
Date of production, publication, distribution, manufacture, or copyright notice 2014.
300 ## - PHYSICAL DESCRIPTION
Extent XII, 352 p. 147 illus.
Other physical details online resource.
336 ## - CONTENT TYPE
Content type term text
Content type code txt
Source rdacontent
337 ## - MEDIA TYPE
Media type term computer
Media type code c
Source rdamedia
338 ## - CARRIER TYPE
Carrier type term online resource
Carrier type code cr
Source rdacarrier
347 ## - DIGITAL FILE CHARACTERISTICS
File type text file
Encoding format PDF
Source rda
490 1# - SERIES STATEMENT
Series statement Theoretical Computer Science and General Issues,
International Standard Serial Number 2512-2029 ;
Volume/sequential designation 9000
505 0# - FORMATTED CONTENTS NOTE
Formatted contents note Introduction -- Motivation -- Overview -- Number Formats and Boolean Algebra -- Basics -- Numbers, Sets and Logical Connectives -- Sequences and Bit-Strings -- Modulo Computation -- Geometric Sums -- Binary Numbers -- Two's Complement Numbers -- Boolean Algebra -- Identities -- Solving Equations -- Disjunctive Normal Form -- Hardware -- Digital Gates and Circuits -- Some Basic Circuits -- Clocked Circuits -- Digital Clocked Circuits -- The Detailed Hardware Model -- Timing Analysis -- Registers -- Drivers and Main Memory -- Open Collector Drivers and Active Low Signal -- Tristate Drivers and Bus Contention -- The Incomplete Digital Model for Drivers -- Self Destructing Hardware -- Clean Operation of Tristate Buses -- Specification of Main Memory -- Operation of Main Memory via a Tristate Bus -- Finite State Transducers -- Realization of Moore Automata -- Precomputing Outputs of Moore Automata -- Realization of Mealy Automata -- Precomputing Outputs of Mealy Automata -- Nine Shades of RAM -- Basic Random Access Memory -- Single-Port RAM Designs -- Read Only Memory (ROM) -- Multi-bank RAM -- Cache State RAM -- SPR RAM -- Multi-port RAM Designs -- 3-port RAM for General Purpose Registers -- General 2-port RAM -- 2-port Multi-bank RAM-ROM -- 2-port Cache State RAM -- Arithmetic Circuits -- Adder and Incrementer -- Arithmetic Unit -- Arithmetic Logic Unit (ALU) -- Shift Unit -- Branch Condition Evaluation Unit -- A Basic Sequential MIPS Machine -- Tables -- I-type -- R-type -- J-type -- MIPS ISA -- Configuration and Instruction Fields -- Instruction Decoding -- ALU-Operations -- Shift Unit Operations -- Branch and Jump -- Sequences of Consecutive Memory Bytes -- Loads and Stores -- ISA Summary -- A Sequential Processor Design -- Software Conditions -- Hardware Configurations and Computations -- Memory Embedding -- Defining Correctness for the Processor Design -- Stages of Instruction Execution -- Initialization -- Instruction Fetch -- Instruction Decoder -- Reading from General Purpose Registers -- Next PC Environment -- ALU Environment.-Shift Unit Environment -- Jump and Link -- Collecting Results -- Effective Address -- Shift for Store Environment -- Memory Stage -- Shifter for Load -- Writing to the General Purpose Register File -- Pipelining.-MIPS ISA and Basic Implementation Revisited -- Delayed PC -- Implementing the Delayed PC -- Pipeline Stages and Visible Registers -- Basic Pipelined Processor Design -- Transforming the Sequential Design -- Scheduling Functions -- Use of Invisible Registers -- Software Condition SC-1 -- Correctness Statement -- Correctness Proof of the Basic Pipelined Design -- Forwarding -- Hits -- Forwarding Circuits -- Software Condition SC-2 -- Scheduling Functions Revisited -- Correctness Proof -- Stalling Stall Engine -- Hazard Signals -- Correctness Statement -- Scheduling Functions -- Correctness Proof -- Liveness -- Caches and Shared Memory -- Concrete and Abstract Caches -- Abstract Caches and Cache Coherence -- Direct Mapped Caches -- k-way Associative Caches -- Fully Associative Caches -- Notation -- Parameters -- Memory and Memory Systems -- Accesses and Access Sequences -- Sequential Memory Semantics -- Sequentially Consistent Memory Systems -- Memory System Hardware Configurations -- Atomic MOESI Protocol -- Invariants -- Defining the Protocol by Tables -- Translating the Tables into Switching Functions -- Algebraic Specification -- Properties of the Atomic Protocol -- Gate Level Design of a Shared Memory System -- Specification of Interfaces -- Data Paths of Caches -- Cache Protocol Automata -- Automata Transitions and Control Signals -- Bus Arbiter -- Initialization -- Correctness Proof -- Arbitration -- Silent Slaves and Silent Masters -- Automata Synchronization -- Control of Tristate Drivers -- Protocol Data Transmission -- Data Transmission -- Accesses of the Hardware Computation -- Relation with the Atomic Protocol -- Ordering Hardware Accesses Sequentially -- Sequential Consistency -- Liveness -- A Multi-core Processor -- Compare-and-Swap Instruction -- Introducing CAS to the ISA -- Introducing CAS to the Sequential Processor -- Multi-core ISA and Reference Implementation -- Multi-core ISA Specification -- Sequential Reference Implementation -- Simulation Relation -- Local Configurations and Computations -- Accesses of the Reference Computation -- Shared Memory in the Multi-core System -- Notation -- Invisible Registers and Hazard Signals -- Connecting Interfaces -- Stability of Inputs of Accesses -- Relating Update Enable Signals and Ends of Accesses -- Scheduling Functions -- Stepping Function -- Correctness Proof -- Liveness -- References -- Index.
520 ## - SUMMARY, ETC.
Summary, etc. This monograph is based on the third author's lectures on computer architecture, given in the summer semester 2013 at Saarland University, Germany. It contains a gate level construction of a multi-core machine with pipelined MIPS processor cores and a sequentially consistent shared memory. The book contains the first correctness proofs for both the gate level implementation of a multi-core processor and also of a cache based sequentially consistent shared memory. This opens the way to the formal verification of synthesizable hardware for multi-core processors in the future. Constructions are in a gate level hardware model and thus deterministic. In contrast the reference models against which correctness is shown are nondeterministic. The development of the additional machinery for these proofs and the correctness proof of the shared memory at the gate level are the main technical contributions of this work.
650 #0 - SUBJECT ADDED ENTRY--TOPICAL TERM
Topical term or geographic name entry element Algorithms.
9 (RLIN) 3390
650 #0 - SUBJECT ADDED ENTRY--TOPICAL TERM
Topical term or geographic name entry element Software engineering.
9 (RLIN) 4138
650 #0 - SUBJECT ADDED ENTRY--TOPICAL TERM
Topical term or geographic name entry element Computers.
9 (RLIN) 8172
650 #0 - SUBJECT ADDED ENTRY--TOPICAL TERM
Topical term or geographic name entry element Microprocessors.
9 (RLIN) 172945
650 #0 - SUBJECT ADDED ENTRY--TOPICAL TERM
Topical term or geographic name entry element Computer architecture.
9 (RLIN) 3513
650 #0 - SUBJECT ADDED ENTRY--TOPICAL TERM
Topical term or geographic name entry element Computer networks .
9 (RLIN) 31572
650 #0 - SUBJECT ADDED ENTRY--TOPICAL TERM
Topical term or geographic name entry element Compilers (Computer programs).
9 (RLIN) 3350
650 14 - SUBJECT ADDED ENTRY--TOPICAL TERM
Topical term or geographic name entry element Algorithms.
9 (RLIN) 3390
650 24 - SUBJECT ADDED ENTRY--TOPICAL TERM
Topical term or geographic name entry element Software Engineering.
9 (RLIN) 4138
650 24 - SUBJECT ADDED ENTRY--TOPICAL TERM
Topical term or geographic name entry element Computer Hardware.
9 (RLIN) 33420
650 24 - SUBJECT ADDED ENTRY--TOPICAL TERM
Topical term or geographic name entry element Processor Architectures.
9 (RLIN) 172946
650 24 - SUBJECT ADDED ENTRY--TOPICAL TERM
Topical term or geographic name entry element Computer Communication Networks.
9 (RLIN) 172947
650 24 - SUBJECT ADDED ENTRY--TOPICAL TERM
Topical term or geographic name entry element Compilers and Interpreters.
9 (RLIN) 31853
700 1# - ADDED ENTRY--PERSONAL NAME
Personal name Müller, Silvia M.
Relator term author.
Relationship aut
-- http://id.loc.gov/vocabulary/relators/aut
9 (RLIN) 172948
700 1# - ADDED ENTRY--PERSONAL NAME
Personal name Paul, Wolfgang J.
Relator term author.
Relationship aut
-- http://id.loc.gov/vocabulary/relators/aut
9 (RLIN) 172949
710 2# - ADDED ENTRY--CORPORATE NAME
Corporate name or jurisdiction name as entry element SpringerLink (Online service)
9 (RLIN) 172950
773 0# - HOST ITEM ENTRY
Title Springer Nature eBook
776 08 - ADDITIONAL PHYSICAL FORM ENTRY
Relationship information Printed edition:
International Standard Book Number 9783319139050
776 08 - ADDITIONAL PHYSICAL FORM ENTRY
Relationship information Printed edition:
International Standard Book Number 9783319139074
830 #0 - SERIES ADDED ENTRY--UNIFORM TITLE
Uniform title Theoretical Computer Science and General Issues,
International Standard Serial Number 2512-2029 ;
Volume/sequential designation 9000
9 (RLIN) 172951
856 40 - ELECTRONIC LOCATION AND ACCESS
Uniform Resource Identifier <a href="https://doi.org/10.1007/978-3-319-13906-7">https://doi.org/10.1007/978-3-319-13906-7</a>
912 ## -
-- ZDB-2-SCS
912 ## -
-- ZDB-2-SXCS
912 ## -
-- ZDB-2-LNC
942 ## - ADDED ENTRY ELEMENTS (KOHA)
Koha item type eBooks-Lecture Notes in CS

No items available.