[openstack-dev] [Openstack] [Heat][convergence] Formal model for SyncPoints
Ryan Brown
rybrown at redhat.com
Wed Feb 11 13:51:18 UTC 2015
Oops, sent this to openstack@ not openstack-dev at .
On 02/10/2015 04:52 PM, Ryan Brown wrote:
> 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
> prototype.
>
> 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.
>
> Cheers,
> Ryan
>
> [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-dev
mailing list