IEEE Transactions on Computers

IEEE Transactions on Computers (TC) is a monthly publication that publishes research in such areas as computer organizations and architectures, digital devices, operating systems, and new and important applications and trends.

Expand your horizons with Colloquium, a monthly survey of abstracts from all CS transactions! Replaces OnlinePlus in January 2017.

From the February 2017 issue

Deadlock Verification of Cache Coherence Protocols and Communication Fabrics

By Freek Verbeek, Pooria M. Yaghini, Ashkan Eghbal, and Nader Bagherzadeh

Featured article thumbnail imageCache coherence plays a major role in manycore systems. The verification of deadlocks is a challenge in particular, because deadlock freedom is an emerging property. Formal methods often decouple verification of the protocol from verification of the communication interconnect. Modern communication fabrics, however, become more advanced and include a network topology, routing, arbitration, synchronization, and more. In this paper, an integrated approach is proposed that allows cross-layer verification of both the cache coherence protocol and the communication fabric all at once. An automated methodology for deriving cross-layer invariants is proposed. These invariants relate the state of the application-layer protocols to en route packets in the communication fabric. Using the invariants, we derive formal proofs of deadlock-freedom for two case studies: a directory-based MI protocol in a 2D mesh, and a ring-based snoopy protocol in a 2D torus. Additionally, we show that our methodology can be used to derive the smallest possible queue sizes that ensure absence of deadlocks. Our methodology is generally applicable and shows promising scalability.

download PDF View the PDF of this article      csdl View this issue in the digital library     TC Featured Article Youtube video  YouTube     TC Featured Article Youtube video in Chinese  YouTube (Chinese)     TC Featured Article on Youku  Youku     TC Featured Article Youtube video in Spanish  YouTube (Spanish)

Editorials and Announcements

Editor's pick of the year 2016 (4 selected papers, each one free-to-download for three months in 2017)


  • Editor's pick of the year selection, announced in the July 2016 Editorial
  • Multimedia presentations of each monthly featured paper are now available in Chinese, English and Spanish
  • Get Your Journals as eBooks for Free



Guest Editorials

Reviewers List

Annual Index

New Essential Set

Access Recently Published TC Articles

RSS Subscribe to the RSS feed of latest TC content added to the digital library

Mail Sign up for the Transactions Connection newsletter.

A Message from Editor-in-Chief Paolo Montuschi


Importance of Coherence Protocols with Network Applications on Multi-Core Processors


Automated Generation of Performance and Dependability Models for the Assessment of Wireless Sensor Networks

Computing Now