Skip to content

Conversation

@xeren
Copy link
Collaborator

@xeren xeren commented Feb 9, 2026

Restructures the LlvmCmpXchg event from #332 into a single-result event using the AggregateType from #493. This was the only event in our IR with two result registers.

Also adds proper compilation of weak LlvmCmpXchg. The intrinsics of pthread_mutex_trylock, pthread_rwlock_tryrdlock and pthread_rwlock_trywrlock now use strong events instead of weak ones. The API seems not to specify these to fail spuriously.

Comment on lines +16 to +18
Preconditions.checkArgument(oldValueAndSuccessRegister.getType() instanceof AggregateType t
&& t.getFields().size() == 2,
"Non-aggregate result register of LlvmCmpXchg.");

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Why not add a check to be sure the part of the aggregate representing the comparison is bool?

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Because it is bv1 when parsed from LLVM IR. During compilation, VisitorBase creates a bool register.

Comment on lines +95 to +96
final var type = e.getResultRegister().getType() instanceof AggregateType t ? t : null;
verify(type != null && type.getFields().size() == 2, "Invalid result type of '%s'", e);

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Why not check directly in the verify that the type is an aggregate?

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Because this method needs type later.

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I don't get it. When you define type you can generate a null (if the instance check does not hold) but then in the verify you do not allow type to be null. Why not simlply

verify(e.getResultRegister().getType() instanceof AggregateType);
verify(e.getResultRegister().getType().getFields().size() == 2, "Invalid result type of '%s'", e);

Copy link
Collaborator

@ThomasHaas ThomasHaas Feb 11, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

He basically says that he wants to avoid doing the the cast to AggregateType part twice:

verify (type instance of AggregateType t && ...)
AggregateType t = (AggregateType) type; // "second" cast
// do something else with "t"

But I would totally prefer the version with the second cast instead of using nulls (null is always ugly).

Comment on lines 875 to 880
return List.of(
spinLoopHead,
newPthreadTryLock(oldValueRegister, successRegister, address, true),
EventFactory.newJump(successRegister, spinLoopEnd),
newPthreadTryLock(oldValueSuccessRegister, address),
EventFactory.newJump(expressions.makeExtract(oldValueSuccessRegister, 1), spinLoopEnd),
EventFactory.newGoto(spinLoopHead),
spinLoopEnd
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I just noticed that our loop unrolling will unroll the spinloop but the dynamic side-effect detection will actually bound the loop to one iteration. I think it would be fair to generate a __VERIFIER_loopbound(1) event here to restrict the loop.
Well, at least if dynamic spin loop detection is enabled... but I think we might want to assume it is enabled?

This optimization could be applied to every CAS-loop that we generate ourselves (if there are more such cases).

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants