Create a gist now

Instantly share code, notes, and snippets.

What would you like to do?
Alloy による Kubernetes のコンテナスケジューリングのモデリング
open util/ordering[Time]
sig Time {}
abstract sig Event {
pre, post : Time,
} {
post = pre.next
}
fact trace {
all t : Time - last | one pre.t
}
sig Identifier {}
sig Node {}
sig Image {}
sig ApiServer {
etcds : some Etcd,
}
sig Etcd {
pods : Pod set -> Time,
replicaSets : ReplicaSet set -> Time,
nodes : Node set -> Time,
}
sig Pod {
label : Identifier,
images : some Image,
scheduledOn : Node lone -> Time,
}
sig ReplicaSet {
selector : disj Identifier,
images : some Image,
replicas : Int,
} {
replicas >= 0
}
sig Container {
image : Image,
runningOn : Node lone -> Time,
}
fact indentity {
all p, p' : Pod | p.label = p'.label => p.images = p'.images
all rs, rs' : ReplicaSet
| rs.selector = rs'.selector => rs.images = rs'.images
all p : Pod, rs : ReplicaSet
| p.label = rs.selector => p.images = rs.images
}
pred etcdInvariant[t, t' : Time, etcds : set Etcd] {
all etcd : etcds {
etcd.pods.t' = etcd.pods.t
etcd.replicaSets.t' = etcd.replicaSets.t
etcd.nodes.t' = etcd.nodes.t
}
}
pred podInvariant[t, t' : Time, pods : set Pod] {
all p : pods | p.scheduledOn.t' = p.scheduledOn.t
}
pred containerInvariant[t, t' : Time, containers : set Container] {
all c : containers | c.runningOn.t' = c.runningOn.t
}
sig CreateReplicaSet extends Event {
apiServer : ApiServer,
replicaSet : ReplicaSet,
} {
all etcd : apiServer.etcds {
etcd.pods.post = etcd.pods.pre
etcd.nodes.post = etcd.nodes.pre
replicaSet not in etcd.replicaSets.pre
etcd.replicaSets.post = etcd.replicaSets.pre + replicaSet
}
podInvariant[pre, post, Pod]
containerInvariant[pre, post, Container]
}
sig ControllerManager extends Event {
apiServer : ApiServer,
replicaSet : ReplicaSet,
modifiedPods : some Pod,
} {
all etcd : apiServer.etcds {
etcd.replicaSets.post = etcd.replicaSets.pre
etcd.nodes.post = etcd.nodes.pre
replicaSet in etcd.replicaSets.pre
let id = replicaSet.selector, desiredNum = replicaSet.replicas,
currentPods = (etcd.pods.pre & label.id),
resultPods = (etcd.pods.post & label.id) {
#currentPods != desiredNum
#currentPods < desiredNum
=> resultPods = currentPods + modifiedPods
#currentPods > desiredNum
=> resultPods = currentPods - modifiedPods
#resultPods = desiredNum
}
}
modifiedPods.scheduledOn.post = none
podInvariant[pre, post, Pod - modifiedPods]
containerInvariant[pre, post, Container]
}
sig Scheduler extends Event {
apiServer : ApiServer,
scheduledPods : some Pod,
} {
all etcd : apiServer.etcds {
scheduledPods in etcd.pods.pre
scheduledPods.scheduledOn.post in etcd.nodes.pre
}
all p : scheduledPods | no p.scheduledOn.pre && some p.scheduledOn.post
etcdInvariant[pre, post, Etcd]
podInvariant[pre, post, Pod - scheduledPods]
containerInvariant[pre, post, Container]
}
sig Kubelet extends Event {
apiServer : ApiServer,
installedOn : Node,
modifiedContainers : some Container,
} {
all etcd : apiServer.etcds, im : Image {
let desiredNum = #(etcd.pods.pre & images.im & scheduledOn.pre.installedOn),
currentCons = (runningOn.pre.installedOn & image.im),
resultCons = (runningOn.post.installedOn & image.im),
targetCons = (modifiedContainers & image.im) {
#currentCons != desiredNum
#currentCons < desiredNum
=> resultCons = currentCons + targetCons
#currentCons > desiredNum
=> resultCons = currentCons - targetCons
#resultCons = desiredNum
}
}
etcdInvariant[pre, post, Etcd]
podInvariant[pre, post, Pod]
containerInvariant[pre, post, Container - modifiedContainers]
}
pred init[t : Time] {
one ApiServer
one Etcd
no Etcd.(pods + replicaSets).t
no Pod.scheduledOn.t
no Container.runningOn.t
}
pred completed[t : Time] {
some rs : ReplicaSet {
rs.replicas = 2
#rs.images = 2
all im : rs.images {
#(runningOn.t.Node & image.im) = rs.replicas
}
}
}
pred scenario {
init[first]
completed[last]
}
run scenario for
4 Int,
6 Time,
5 Event,
1 Identifier,
2 Node,
2 Image,
1 ApiServer,
1 Etcd,
2 Pod,
1 ReplicaSet,
4 Container
<?xml version="1.0"?>
<alloy>
<view>
<projection> <type name="Time"/> </projection>
<defaultnode/>
<defaultedge color="Black"/>
<node>
<type name="ApiServer"/>
<type name="ControllerManager"/>
<type name="CreateReplicaSet"/>
<type name="Etcd"/>
<type name="Int"/>
<type name="Kubelet"/>
<type name="Scheduler"/>
<type name="String"/>
<type name="Time"/>
<type name="ordering/Ord"/>
<type name="seq/Int"/>
<set name="$completed_rs" type="ReplicaSet"/>
<set name="First" type="ordering/Ord"/>
<set name="Next" type="ordering/Ord"/>
<set name="post" type="Event"/>
<set name="pre" type="Event"/>
</node>
<node color="White">
<type name="univ"/>
</node>
<node hideunconnected="yes">
<type name="Container"/>
<type name="Event"/>
<type name="Identifier"/>
<type name="Image"/>
<type name="Node"/>
</node>
<node hideunconnected="yes" style="Dashed">
<type name="Pod"/>
</node>
<node hideunconnected="yes" style="Dashed" color="White">
<type name="ReplicaSet"/>
</node>
<edge visible="no" attribute="yes">
<relation name="apiServer"> <type name="ControllerManager"/> <type name="ApiServer"/> </relation>
<relation name="apiServer"> <type name="CreateReplicaSet"/> <type name="ApiServer"/> </relation>
<relation name="apiServer"> <type name="Kubelet"/> <type name="ApiServer"/> </relation>
<relation name="apiServer"> <type name="Scheduler"/> <type name="ApiServer"/> </relation>
<relation name="image"> <type name="Container"/> <type name="Image"/> </relation>
<relation name="images"> <type name="Pod"/> <type name="Image"/> </relation>
<relation name="images"> <type name="ReplicaSet"/> <type name="Image"/> </relation>
<relation name="installedOn"> <type name="Kubelet"/> <type name="Node"/> </relation>
<relation name="label"> <type name="Pod"/> <type name="Identifier"/> </relation>
<relation name="modifiedContainers"> <type name="Kubelet"/> <type name="Container"/> </relation>
<relation name="modifiedPods"> <type name="ControllerManager"/> <type name="Pod"/> </relation>
<relation name="nodes"> <type name="Etcd"/> <type name="Node"/> </relation>
<relation name="replicas"> <type name="ReplicaSet"/> <type name="Int"/> </relation>
<relation name="replicaSet"> <type name="ControllerManager"/> <type name="ReplicaSet"/> </relation>
<relation name="replicaSet"> <type name="CreateReplicaSet"/> <type name="ReplicaSet"/> </relation>
<relation name="scheduledPods"> <type name="Scheduler"/> <type name="Pod"/> </relation>
<relation name="selector"> <type name="ReplicaSet"/> <type name="Identifier"/> </relation>
</edge>
</view>
</alloy>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment