9fans archive / 1997 / 04 / 72 /    prev next

From: miller@ham... miller@ham...
Subject: Pentium Pro and coherence
Date: Mon, 21 Apr 1997 22:18:21 BST

I'm sorry if my clumsy editing gave the impression that my summary
of the content of a message from presotto@pla...:

	> [a fascinating account of how the Pentium Pro's out-of-order
	> instruction execution breaks the Plan 9 sleep/wakeup code on
	> a multi-CPU system]

was meant to be a direct quote.  The words in editorial square brackets
are mine, not his.  I haven't quite got the hang of this new-fangled
electronical mailing business ...

Anyway, it is certainly plausible that speculative reads are the
problem.  The essential bit of code seems to be the equivalent of the 
following fragment of Alef:

	par {
		{ a = 1; x = b; }
		{ b = 1; y = a; }
	}

It is `obvious' that this establishes the postcondition (x==1 || y==1).
Informal proof: if not (x==1), then (x=b) must have been executed before
(b=1), and therefore (a=1) must have been executed before (y=a), so that
we must have (y==1).  But this reasoning depends on the left-to-right
ordering of sequential assignments.  If that's not guaranteed on the
Pentium Pro, then shared-variable concurrency without locks becomes
very scary indeed.

presotto@pla... writes [his words this time]:

> Forcing an interlock
> at both the beginning and end of a locked section seems to be
> pretty conservative to me [...] The
> truth is that we have no way of knowing whether we're conservative
> enough.

I hope this is overly pessimistic.  In order for locked critical
sections to work at all, the hardware must be able to guarantee
that the ordering of effects before and after the locking instruction
will be preserved.  Or is this too naive?

-- Richard Miller