Samuel Tardieu wrote:
On 26/10, Robert Dewar wrote:
| Of course in Ada there is a clear notion of threads semantic, and
| a clear definition of what the meaning of code is in the presence
| of threads, so the specific situation discussed here is easy to
| deal with (though Ada takes the view that unsychronized shared access to
| non-atomic or non-volatile data from separate threads has undefined
| effects).
In the following example, is the access to "Shared" considered
unsynchronized even though what looks like a proper lock is used
around it?
Yes, it is unsynchronized. Why would you think otherwise? (referencing
the RM). You can't adopt a naive memory model in Ada! One way to think
about things is that tasks are free to keep local copies of all global
variables, synchronizing their values only at a point of
synchronization. Locking of this kind needs to be done with
entry barriers.
package P is
Shared : Natural := 0;
procedure Maybe_Increment;
end P;
package body P is
protected Lock is
procedure Maybe_Lock (Locked : out Boolean);
procedure Always_Unlock;
private
Is_Locked : Boolean := False;
end Lock;
protected body Lock is
procedure Always_Unlock is
begin
Is_Locked := False;
end Always_Unlock;
procedure Maybe_Lock (Locked : out Boolean) is
begin
Locked := not Is_Locked;
Is_Locked := True;
end Maybe_Lock;
end Lock;
procedure Maybe_Increment is
L : Boolean;
begin
Lock.Maybe_Lock (L);
if L then
Shared := Shared + 1;
end if;
Lock.Always_Unlock;
end Maybe_Increment;
end P;
By naively reading the code, I would assume that if two tasks were to
call Maybe_Increment once, after completion of those tasks Shared would
contain either 1 or 2, depending on whether they both got the lock in
turn or if only one of them got it.
However, if you look at the x86 code for Maybe_Increment (-O3
-fomit-frame-pointer -fno-inline), you'll see:
1 p__maybe_increment:
2 .LFB11:
3 subl $12, %esp
4 .LCFI6:
5 movl $p__lock, %eax
6 call p__lock__maybe_lockP
7 cmpb $1, %al
8 movl p__shared, %eax <=== unconditional load
9 sbbl $-1, %eax <=== conditional +1
10 movl %eax, p__shared <=== unconditional store
11 movl $p__lock, %eax
12 addl $12, %esp
13 jmp p__lock__always_unlockP
Note lines 8 to 10: on a multiprocessor system with both tasks running at
the same time on different processors, you can end up with Shared being
zero after the two tasks have ended (for example if the task getting the
lock runs one or two instructions ahead the one without the lock).
Sam
