[Openstack] [Heat][convergence] Formal model for SyncPoints

Ryan Brown rybrown at redhat.com
Tue Feb 10 21:52:23 UTC 2015

Heat team,

After looking at Zane's prototype[1] and the ML threads on SyncPoint, I
thought it'd be helpful to make a model of *just* the logic around
resource locking. Hopefully, it'll help during implementation to be able
to see just the logic without the stubbed-out data store etc from the

The model[2] is the absolute minimum I could implement and still capture
what syncpoints are supposed to do. A stack is still a collection of
resources, but resources themselves are reduced to just their IDs. Locks
are still at the resource level and dependency trees are followed as in
Zane's prototype.

Modeling it has confirmed the things we've already worked out about
SyncPoints and sharing workload across workers. Resource-level locking
is the best granularity for workers, and there isn't a case the model
checker was able to generate that breaks the resource dependency order
or ends with multiple holders of a given SyncPoint.

It also confirms that the architecture we have is going to have serious
database overhead for managing these locks. We've been over that, and
there isn't much of a way around it without adding some other shared
synchronization system.

If you'll be implementing convergence, please take a read over the PDF
version[3] and feedback/questions are (of course) welcome.


[1]: https://github.com/zaneb/heat-convergence-prototype/tree/resumable
[2]: https://github.com/ryansb/heat-tla-model
[3]: https://github.com/ryansb/heat-tla-model/blob/master/Heat.pdf

Ryan Brown / Software Engineer, Openstack / Red Hat, Inc.

More information about the Openstack mailing list