Surprising code generated for vdso_read_begin()

[Christophe Leroy]

Wondering why we get something so complicated/redundant for 
vdso_read_begin() <include/vdso/helpers.h>

static __always_inline u32 vdso_read_begin(const struct vdso_data *vd)
{
	u32 seq;

	while ((seq = READ_ONCE(vd->seq)) & 1)
		cpu_relax();

	smp_rmb();
	return seq;
}


 6e0:   81 05 00 f0     lwz     r8,240(r5)
 6e4:   71 09 00 01     andi.   r9,r8,1
 6e8:   41 82 00 10     beq     6f8 <__c_kernel_clock_gettime+0x158>
 6ec:   81 05 00 f0     lwz     r8,240(r5)
 6f0:   71 0a 00 01     andi.   r10,r8,1
 6f4:   40 82 ff f8     bne     6ec <__c_kernel_clock_gettime+0x14c>
 6f8:

r5 being vd pointer

Why the first triplet, not only the second triplet ? Something wrong 
with using READ_ONCE() for that ?

Christophe