两个urgent location引发deadlock的问题解决方案咨询

这类死锁的本质是：urgent位置会冻结全局时间推进，仅允许瞬时迁移触发，当两个并发进程同时满足urgent位置的进入/停留条件、且各自的迁移触发条件互相依赖对方的动作或时间推进时，就会出现循环等待的死锁场景

可参考以下方案针对性解决：

• 对依赖关系明确的并发进程，添加优先级标注：给等待路径更短、或者和时间上界验证强相关的进程的urgent迁移设置更高优先级，确保高优先级迁移先触发，打破循环等待。注意优先级设置不能修改你要验证的时间上下界逻辑，仅用来解决同时间点的迁移冲突。
• 拆分urgent位置的瞬时逻辑：把原来的单个urgent位置拆分为「预检查位置」+「实际urgent位置」，在预检查位置先判断另一侧进程的状态，如果对方也即将进入urgent位置，先触发同步通道完成状态协商，再进入真正的urgent位置执行后续逻辑。
• 增加瞬时同步通道：为两个可能同时进入urgent位置的进程添加一对空的同步通道urg_sync!和urg_sync?，要求任意进程进入urgent位置前必须先完成一次同步，确保同一时间点只有一个进程能进入urgent相关逻辑，从根源上避免并发冲突。
• 边界场景特判：如果死锁仅出现在你要验证的时间上下界的极限值位置，可以在验证属性中添加边界条件过滤，比如你的时间上界是T，就给属性加上t < T的前置判定，避免极限边界的死锁影响整体验证结果的正确性。

注意：所有修改都需要先做一致性验证，确保修改后的模型和原模型的时间可达性逻辑完全一致，不会影响你最终要验证的时间上下界结论。

内容的提问来源于stack exchange，提问作者eric