X86_64 Memory Type Tests

This document explores the effect of X86_64 memory types on memory model. This is companion material to our article “Extending Intel-x86 Consistency and Persistency: Formalising the Semantics of Intel-x86 Memory Types and Non-Temporal Stores” by A. Raad, L. Maranget, V. Vafeiadis.

Some files are provided: model (NEW.cat), models output (TSO, Model), consolidated hardware logs (Hardware) and litmus tests (src.tgz).

Amongst many, we present our main experimental result in section Comparing hardware with the model: our model is not invalidated by experiments.

• Reproduce some experiments
  • Main experiment: comparing model and hardware logs
  • Advanced experiment: running tests on hardware
• Test base and hardware description
• Comparing hardware with the model
  • Invalid behaviours
  • Behaviours allowed by the model and not observed
• Comparing hardware results with classical models
• Specific experiments
  • Uncached memory type and SC
  • Write combine memory type and the message passing litmus test
  • Write combine memory type and the store buffer litmus test
  • Write combine memory type and the TSO model
• Write to Read relaxations
  • Read into uncached memory type
  • Read into write combining memory type
  • Read into write back memory type
  • Read into write through memory type
• Read to Read relaxations
• Read to Write relaxations
• Write to write relaxations
  • All write to Write tests
  • Presentation by tests
• Restoring SC (or not)
  • Simple SC violations
  • With atomic exchange
  • With fences
  • With sfences
• Coherence
• Testing the clflush instruction
  • Series 00
  • Series 01
  • Series 02
  • Series 03
  • Series 05
  • Series 06
  • Series 07
  • Series 08
  • Series 09
  • Series 10
  • Series 14
  • Series 15
  • Series 16
  • Series 17
  • All clflush and clflushopt variations in between write-to-write
• Instruction clflushopt acts differentlty from instruction clflush
• Specific behaviours for each machine
  • CoreI5-dual
  • CoreI5
  • CoreI7
  • Chianti
  • Limoux
  • Teraram
  • Estephe
  • Barsac
  • Zdani
• Miscellaneous
  • Compare exchange
  • All writes in test are non-temporal writes (two thread tests)
• New this round

This document was translated from L^AT_EX by H^EV^EA.