remove SynchronizeEventSet?

[jmdyck]

The spec defines SynchronizeEventSet, but never references it. Should it be removed? (Or is there somewhere that should be referencing it, but isn't?)

[syg]

Good question. It was added in ef0cf19 as part of the fix for wait-notify synchronization.

Perhaps @conrad-watt initially meant to filter out the synchronization events from the main event set, and then opted to do it via a [[AgentSynchronizesWith]] list directly? Conrad, can you confirm?

If so, we can delete it.

[conrad-watt]

I think it was orphaned after I inlined some definitions in response to this comment on the PR.

Sorry for not noticing!

[syg]

Makes sense. Removal sgtm.

[jaag5678]

To my understanding and comment on this. I think [AgentSynchronizesWith] should be replaced by synchronize event set. Cause there would be many points where multiple agents are going to synchronize with each other and therefore have a happens-before relation between their shared data block events. The naming AgentSynchronizesWith sounds misleading compared to Synchronize event sets which explicitly constrain ordering between events.

Any comment on this?

[syg]

@jaag5678 To clarify, you're asking for an editorial change, correct? Do you have a particular editorial change in mind?

It is true that the event pairs in an [[AgentSynchronizesWith]] list are going to be from different agent. I guess I don't find it particularly misleading because with "SynchronizesWith" as part of the name, I'd expect it to contain different agents.

[conrad-watt]

My original reasoning for the [[AgentSynchronizesWith]] field name was that it records operationally-determined outgoing synchronization edges on a per-agent basis (from that agent specifically, to other agents). An reasonable alternative scheme would be having an [[AdditionalSynchonizesWith]] record field directly in the [[CandidateExecution]], which holds all the synchronization edges at once, to avoid the per-agent style (similar to [[HostSynchronizesWith]]).

In both cases, the field would be a list of pairs. @jaag5678, is your main concern the name, or do you think the representation should be changed (involving a set)?

[jaag5678]

Hi there,

Let me explain what is my intuition behind this.

• The name [[AgentSynchronizesWith]] at first glance is not something that hints at the pairs of events that are synchronized. Which is why I think we would need something as Synchronize Event Set to persist to explain what it is.

• The confusion could come due to the fact that the Agents Synchronize as a consequence due to two events synchronizing which belong to respective agents. However, the core fact remains that two events are synchronizing with each other. This is why I felt that Synchronize event set should remain.

• @syg I am asking if an editorial change is possible that retain the Synchronize Event set and introduce a function that gives us the [[AgentSynchronizesWith]] list as per @conrad-watt mentioned. Cause if I am not wrong, reading the record field description of [[AgentSynchronizesWith]] gives me not much insight on the per-agent-basis and especially not the outward going edges from the particular agent as what @conrad-watt mentions.

• @conrad-watt The representation could be changed to a set of pairs if the list that is described for [[AgentSynchronizesWith]] is not necessarily an ordered one. Correct me if I am wrong but is there any other advantage of list over set?

Let me know what you think of what I mentioned above. Or if I have missed some details from the spec that I have mentioned to be not existent.

Sincerely,
jaag5678

[conrad-watt]

The name [[AgentSynchronizesWith]] at first glance is not something that hints at the pairs of events that are synchronized. Which is why I think we would need something as Synchronize Event Set to persist to explain what it is.
...
@syg I am asking if an editorial change is possible that retain the Synchronize Event set and introduce a function that gives us the [[AgentSynchronizesWith]] list as per @conrad-watt mentioned.

I don't think the SynchronizeEventSet function gives any insight into the design of the model, especially since, as noted, it's not used anywhere. I don't have a clear understanding of what new function you think should be introduced.

... reading the record field description of [[AgentSynchronizesWith]] gives me not much insight on the per-agent-basis and especially not the outward going edges from the particular agent as what @conrad-watt mentions.

I agree that the explanatory note for the [[AgentSynchronizesWith]] record field could be more descriptive, incorporating some of the motivation I posted above. Would this satisfy your concerns?

@conrad-watt The representation could be changed to a set of pairs if the list that is described for [[AgentSynchronizesWith]] is not necessarily an ordered one. Correct me if I am wrong but is there any other advantage of list over set?

Either works, but lists are used by convention for collections which need to be manipulated directly by the operational semantics.

[jaag5678]

@conrad-watt Yes the record could be more descriptive. That would do.

Thanks,
jaag5678