Alloy による Kubernetes のコンテナスケジューリングのモデリング

alloy_kubernetes.als

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

alloy_kubernetes.thm

<?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>