This article pursues speedy packet classification with low on-chip memory requirements realized on Xilinx Virtext-6 FPGA. Based on hashing round-down prefixes specified in filter rules (dubbed HaRP), our implemented classifier is demonstrated to exhibit an extremely low on-chip memory requirement (lowering the byte count per rule by a factor of 8.6 in comparison with its most recent counterpart [2]), taking only 50% of Virtex-6 on-chip memory to store every large rule dataset (with some 30K rules) examined. In addition, it achieves a higher throughput than any known FPGA implementation, reaching more than 200 MPPS (millions packet lookups per second) with 8 processing units and 8 memory banks in the HaRP pipeline to support the line rate over 130 Gbps under bi-directional traffic in the worst case with 40-byte packets. By reducing memory probes per lookup, enhanced HaRP can further boost the classification speed to 255 MPPS.

We present a distinct longest prefix matching (LPM) lookup scheme able to achieve exceedingly concise lookup tables (CoLT), suitable for scalable routers. Based on unified hash tables for handling both IPv4 and IPv6 simultaneously, CoLT excels over previous mechanisms in: 1) lower on-chip storage for lookup tables; 2) simpler table formats to enjoy richer prefix aggregation and easier implementation; and 3) most importantly, deemed the only design able to accommodate both IPv4 and IPv6 addresses uniformly and effectively. As its hash tables permit multiple possible buckets to hold each prefix (following a migration rule to avoid false positives altogether), CoLT exhibits the best memory efficiency and can launch parallel search over tables during every LPM lookup, involving fewer cycles per lookup when on-chip memory is used to implement hash tables. With 16 (or 32) on-chip SRAM blocks clocked at 500 MHz (achievable in today's 65-nm technology), it takes 2 (or 1.6) cycles on average to complete a lookup, yielding 250 (or 310+) millions of packets per second (MPPS) mean throughput. Being hash-oriented, CoLT well supports incremental table updates, besides its high table utilization and lookup throughput.

Packet classification is central to a wide array of Internet applications and services, with its approaches mostly involving either hardware support or optimization steps needed by software-oriented techniques (to add precomputed markers and insert rules in the search data structures). Unfortunately, an approach with hardware support is expensive and has limited scalability, whereas one with optimization fails to handle incremental rule updates effectively. This work deals with rapid packet classification, realized by hashing round-down prefixes (HaRP) in a way that the source and the destination IP prefixes specified in a rule are rounded down to “designated prefix lengths” (DPL) for indexing into hash sets. HaRP exhibits superb hash storage utilization, able to not only outperform those earlier software-oriented classification techniques but also well accommodate dynamic creation and deletion of rules. HaRP makes it possible to hold all its search data structures in the local cache of each core within a contemporary processor, dramatically elevating its classification performance. Empirical results measured on an AMD 4-way 2.8 GHz Opteron system (with 1 MB cache for each core) under six filter data sets (each with up to 30 K rules) obtained from a public source unveil that HaRP enjoys up to some 3.6× throughput level achievable by the best known decision tree-based counterpart, HyperCuts (HC).

This work deals with an architectural framework to enable application-layer packet processing for lowered processing latency and enhanced throughput. Creating an "Ethereal memory" shared by application programs and network interface drivers, the proposed framework realizes application-layer packet processing through Ethereal memory (APPEAL). Unlike earlier solutions based on network processors or field programmable gate arrays, APPEAL supports packet processing software execution in regular OS environments (like Linux) on general-purpose multi-core processors (like Intelreg Core 2 Extreme and Broadcom BCM1480 SoC products). It facilitates fast packet processing code development and lets applications have direct accesses to data contained in Ethereal memory, totally eliminating the need of packet copies between user space and kernel space and of system calls. Without kernel overhead during application layer packet processing, APPEAL is shown by our empirical results obtained from a hardware platform comprising three BCM 1480 SoC's, to enjoy far smaller latency (dropped by as much as 58%) and to more than double throughput, when carrying out network address and port translation.

This article deals with communication performance of a multiprocessor system implemented using award-wining BCM 1480 multi-core chips. Our system uses high-performance HyperTransport links to interconnect constituent chips, realizing cache-coherent non-uniform memory access. It takes advantage of hardware support from the BCM 1480 chip to attain very impressive communication performance among constituent BCM 1480 chips. This is achieved via an extension to global memory, so that small messages can be pushed quickly across chips in less than one us by the CPU cores through DMA to achieve zero-copy message buffering. It eliminates all overhead associated with the kernel and protocol processing for the utmost interconnect bandwidth in data transfers.

This article deals with a novel architecture for IP routing table construction, on the basis of a single set-associative hash table to support fast longest prefix matching (LPM). The proposed architecture uses two key techniques to lower table storage required drastically: (1) storing transformed prefix representations and (2) accommodating multiple prefixes per table entry via prefix aggregation. Given a set of chosen prefix lengths (called "treads"), all prefixes are rounded down to nearest treads before hashed to the table using their transformed representations so that prefix aggregation opportunities abound in hash entries. Significant table storage reduction makes it possible to fit a large routing table in on-chip SRAM, solving both the memory and bandwidth- intensive problems faced by IP routing. Simulation results on real routing tables show that the proposed architecture saves at least two folds of storage when compared with most known hash table- based design or trie-based design. In addition, our design enjoys fast lookups and incremental updates, with the worst-case lookup time upper-bounded theoretically by the number of treads (zeta) but found experimentally to be 4 memory accesses when zeta equals 8.

State-based, formal methods have been successfully applied to the automatic verification of cache coherence in sequentially consistent systems. However, coherence in shared memory multiprocessors under a relaxed memory model is much more complex to verify automatically. With relaxed memory models, incoming invalidations and outgoing updates can be delayed in each cache while processors are allowed to race ahead. This buffering of memory accesses considerably increases the amount of state in each cache and the complexity of protocol interactions. Moreover, because caches can hold inconsistent copies of the same data for long periods of time, coherence cannot be verified by simply checking that cached copies are identical at all times. This paper makes two major contributions. First, we demonstrate how to model and verify cache coherence under a relaxed memory model in the context of state-based verification methods. Frameworks for modeling the hardware and for generating correct memory access sequences driving the hardware model are developed. We also show correctness properties which must be verified on the hardware model. Second, we demonstrate a successful application of a state-based verification tool called SSM for the verification of the delayed protocol, an aggressive protocol for relaxed memory models. SSM is based on an abstraction technique preserving the properties to verify. We show that with classical, explicit approaches the verification of cache coherence is realistically unfeasible because of the state space explosion problem, whereas SSM is able to verify protocols both at both behavioral and message-passing levels.

Directory-based coherence protocols in shared-memory multiprocessors are so complex that verification techniques based on automated procedures are required to establish their correctness. State enumeration approaches are well-suited to the verification of cache protocols but they face the problem of state space explosion, leading to unacceptable verification time and memory consumption even for small system configurations. One way to manage this complexity and make the verification feasible is to map the system model to verify onto a symbolic state model (SSM). Since the number of symbolic states is considerably less than the number of system states, an exhaustive state search becomes possible, even for large-scale sytems and complex protocols. In this paper, we develop the concepts and notations to verifiy some properties of a directory-based protocol designed for non-FIFO interconnection networks. We compare the verification of the protocol with SSM and with the Stanford Mur φ, a verification tool enumerating system states. We show that SSM is much more efficient in terms of verification time and memory consumption and therefore holds that promise of verifying much more complex protocols. A unique feature of SSM is that it verifies protocols for any system size and therefore provides reliable verification results in one run of the tool.

This paper describes the methods used to formulate and validate the memory subsystem of the cache-coherent Sun Scalable Shared-memory MultiProcessor (S3.mp) at three levels of abstraction: the memory consistency model, the cache coherence protocol, and the implementation.

Current high performance computer systems use complex, large superscalar CPUs that interface to the main memory through a hierarchy of caches and interconnect systems. These CPU-centric designs invest a lot of power and chip area to bridge the widening gap between CPU and main memory speeds. Yet, many large applications do not operate well on these systems and are limited by the memory subsystem performance.This paper argues for an integrated system approach that uses less-powerful CPUs that are tightly integrated with advanced memory technologies to build competitive systems with greatly reduced cost and complexity. Based on a design study using the next generation 0.25µm, 256Mbit dynamic random-access memory (DRAM) process and on the analysis of existing machines, we show that processor memory integration can be used to build competitive, scalable and cost-effective MP systems.We present results from execution driven uni- and multi-processor simulations showing that the benefits of lower latency and higher bandwidth can compensate for the restrictions on the size and complexity of the integrated processor. In this system, small direct mapped instruction caches with long lines are very effective, as are column buffer data caches augmented with a victim cache.

We introduce a cache protocol verification technique based on a symbolic state expansion procedure. A global Finite State Machine (FSM) model characterizing the protocol behavior is built and protocol verification becomes equivalent to finding whether or not the global FSM may enter erroneous states. In order to reduce the complexity of the state expansion process, all the caches in the same state are grouped into an equivalence class and the number of caches in the class is symbolically represented by a repetition constructor. This symbolic representation is partly justified by the symmetry and homogeneity of cache-based systems. However, the key idea behind the representation is to exploit a unique property of cache coherence protocols: the fact that protocol correctness is not dependent on the exact number of cached copies. Rather, symbolic states only need to keep track of whether the caches have 0, 1, or multiple copies. The resulting symbolic state expansion process only takes a few steps and verifies the protocol for any system size. Therefore, it is more efficient and reliable than current approaches. The verification procedure is first applied to the verification of five existing protocols under the assumption of atomic protocol transitions. A simple snooping protocol on a split-transaction shared bus is also verified to illustrate the extension of our approach to protocols with nonatomic transitions.>

The complexity of directory based protocols has motivated us to build a hardware emulator or testbed for the rapid prototyping of various protocols under various memory consistency models for CC-NUMA architectures. To implement and verify new protocols rapidly on the testbed, we have developed an overall methodology around a set of tools applicable to different aspects of the verification of a protocol, i.e., protocol-intrinsic errors, memory access ordering errors and protocol implementation errors. These tools include formal verification techniques, architecture simulators and hardware mechanisms implemented in the FPGAs of the testbed.

In this paper we introduce a verification technique for cache coherence protocols at the behavior level. Protocols are specified by a Finite State Machine (FSM) model. The global state space is the Cartesian product of an arbitrary number of individual cache state spaces and is symbolically expanded. A global FSM characterizing the protocol behavior is built and protocol verification becomes equivalent to finding whether or not the global FSM may enter erroneous states. State expansion only takes a few steps, contrary to current approaches. The verification procedure is applied to the verification of five existing protocols Keywords: cache coherence protocol, formal verification, finite state machine, symbolic expansion and shared-memory multiprocessor. 2 The Verification of Cache Coherence Protocols Abstract In this paper we introduce a verification technique for cache coherence protocols at the behavior level. Protocols are specified by a Finite State Machine (FSM) model. The globa...