Why3: Efficient Implementation of Software Concepts

Recall the Alloy specification of the Notifications software concept and its WhyML implementation based on finite sets:

sig Event {}
sig User {
        var subscriptions : set Event,
        var notifications : set Event 
}

pred subscribe [u : User, e : Event] { // Subscribe to an event
        e not in u.subscriptions
        subscriptions' = subscriptions + u->e
        notifications' = notifications
}
pred read [u : User] { // Read all notifications
        some u.notifications
        notifications' = notifications - u->Event
        subscriptions' = subscriptions
}
... 

We implemented this as shown below:

type user = int   type event = int
clone set.SetImp with type elt = (user,event)    

type stateT = { subscriptions: set ; notifications : set }
val state : stateT

let subscribe (u:user) (e:event)
    requires { not mem (u,e) state.subscriptions }
    ensures  { state.subscriptions = add (u,e) (old state.subscriptions) } 
    ensures  { state.notifications = old state.notifications }
  = 
  add (u,e) state.subscriptions

let read (u:user) 
    requires { exists e:event . mem (u,e) state.notifications }
            (* notifications' = notifications - u->Event *)
    ensures  { forall x:user. x <> u -> 
                 (forall e :event. mem (x,e) state.notifications 
                    <-> mem (x,e) (old state.notifications)) }
    ensures  { forall e:event . not mem (u,e) state.notifications }
    ensures  { state.subscriptions = old state.subscriptions }
  =
  let aux = copy state.notifications in
  while not is_empty aux do
    let (x,y) = choose_and_remove aux in
    if x = u then remove (x,y) state.notifications
  done
...

Separate Abstract Specifications

An alternative, more abstract approach would be to write the specification in a dedicated module separate from the implementation:

module Notification_Spec 
  use export int.Int
  use export set.Fset
  type user = int  type event = int
 
  type stateAT = { subscriptions : fset (user,event)  ; 
                   notifications : fset (user,event) }

  predicate subscribe_spec (u:user) (e:event) (s s' :stateAT) = 
     (not mem (u,e) s.subscriptions) 
      -> 
     s'.subscriptions == add (u,e) s.subscriptions /\ 
     s'.notifications == s.notifications 

  predicate unsubscribe_spec (u:user) (e:event) (s s' :stateAT) = 
     mem (u,e) s.subscriptions 
      -> 
     s'.subscriptions == remove (u,e) s.subscriptions /\ 
     s'.notifications == remove (u,e) s.notifications 

  predicate read_spec (u:user) (s s' :stateAT) = 
     (exists e :event. mem (u,e) s.notifications) 
       -> 
      s'.subscriptions == s.subscriptions /\ 
     (forall e :event . not mem (u,e) s'.notifications) /\ 
     (forall x :user. x <> u -> 
        (forall e :event. mem (x,e) s'.notifications <-> mem (x,e) s.notifications))
  ...
end

Then the implementation module will begin as follows, where a concrete implementation type is defined together with an abstraction (or refinement) function from the concrete type to the abstract type:

module Notification_Set
  use Notification_Spec    
  clone set.SetImp with type elt = (user,event)

  type stateT = { subscriptions_ : set ; notifications_ : set }
  function view (s:stateT) : stateAT =
    { subscriptions = to_fset s.subscriptions_ ;
      notifications = to_fset s.notifications_
    }

  val state : stateT

The function definitions are the same as before, but their specifications are simplified to a single postcondition as follows:

  let subscribe (u:user) (e:event)
    ensures  { subscribe_spec u e (old view state) (view state) } 
  = 
    add (u,e) state.subscriptions_


  let read (u:user) 
    ensures  { read_spec u (old view state) (view state) } 
  =
  let aux = copy state.notifications_ in
  while not is_empty aux do
    invariant { forall x:user . x <> u -> forall e :event. 
            mem (x,e) state.notifications_ <-> mem (x,e) (old state.notifications_) }
    invariant { forall e:event . mem (u,e) state.notifications_ -> mem (u,e) aux }
    variant { cardinal aux }
    let (x,y) = choose_and_remove aux in
    if x = u then remove (x,y) state.notifications_
  done

[permalink]

Note that preconditions could still be included if desired. For instance, invocations of read when user u has no notifications to read are innocuous, so in the above version the corresponding precondition is omitted, which means that function calls are allowed when u has nothing to read. But if we wish to disallow this it suffices to include:

    requires { exists e:event . mem (u,e) state.notifications_ } 

This still yields a correct implementation with respect to the read_spec specification.

An Efficient Implementation

Clearly the above implementation of read is not efficient, since it iterates over all pairs (user, event) in **state.notifications_.

A more efficient implementation would give direct access to the event notifications of a given user, for instance storing notifications as a finite map from users to lists of events. Similarly, subscriptions could be stored as a map, but observe that it would make more sense to store them as a finite map from events to lists of users, to facilitate notifying subscribers in the occur action.

We implement this idea in the following module:

module Notifications_List
  use Notification_Spec

  (* type of maps from events to lists of users *)
  clone fmap.MapImp as EventMap with type key = event 
  type eventMapUsers = EventMap.t (list user)

  (* type of maps from users to lists of events *)
  clone fmap.MapImp as UserMap with type key = user
  type userMapEvents = UserMap.t (list event)

  type stateT = { subscriptions_ : eventMapUsers ; notifications_ : userMapEvents }
    invariant { forall u :user, e :event. 
                  EventMap.mem e subscriptions_ -> num_occ u (subscriptions_ e) <= 1 }   
    invariant { forall u :user, e :event. 
                  UserMap.mem u notifications_ -> num_occ e (notifications_ u) <= 1 }   
    by { subscriptions_ = EventMap.create() ; notifications_ = UserMap.create() }


  val function view (s:stateT) : stateAT
    ensures { forall u :user, e :event. 
                Notification_Spec.mem (u,e) result.subscriptions <->
                EventMap.mem e s.subscriptions_ /\ mem u (s.subscriptions_ e) }
    ensures { forall u :user, e :event. 
                Notification_Spec.mem (u,e) result.notifications <->
                UserMap.mem u s.notifications_ /\ mem e (s.notifications_ u) }

  val state : stateT

The type definition includes two invariants. These are not meant as high-level properties, but rather, crucially, as implementation invariants to ensure an adequate realization of binary relations: (user, event) pairs should not occur more than once.

Note also that the view function is specified by means of two postconditions (which is equivalent to writing two axioms for it). Since the maps used in the implementation are finite (and will be extracted to hash tables), lookup operations require checking that the key is in the domain.

The subscribe action function must check if there exists already an entry for the event e in the subscriptions dictionary, and create one if not. Then u can be pushed to that list:

  let subscribe (u:user) (e:event)
    requires { not mem u (state.subscriptions_ e) }
    ensures  { subscribe_spec u e (old view state) (view state) } 
  =
  if not (EventMap.mem e state.subscriptions_)
    then EventMap.add e Nil state.subscriptions_ ; 
  let updsubs = Cons u (EventMap.find e state.subscriptions_) in 
  EventMap.add e updsubs state.subscriptions_

Note the presence of a precondition, required to ensure that the type invariant is preserved .

And here is a possible implementation of unsubscribe . Observe that the user may not have any notifications (and an entry in the notifications dictionary) at this point:

  let unsubscribe (u:user) (e:event)
    requires { EventMap.mem e state.subscriptions_ /\ mem u (state.subscriptions_ e) }
    ensures  { unsubscribe_spec u e (old view state) (view state) } 
  =   
  let updsubs = delete u (EventMap.find e state.subscriptions_) in
  EventMap.add e updsubs state.subscriptions_ ;
  if UserMap.mem u state.notifications_ then 
    let updnotifs = delete e (UserMap.find u state.notifications_) in 
    UserMap.add u updnotifs state.notifications_ 

An alternative implementation might not assume that user u subscribes to event e . This is ok, but the function must then check if an entry of e exists in the state.subscriptions_ dictionary:

  let unsubscribe (u:user) (e:event)
    ensures  { unsubscribe_spec u e (old view state) (view state) } 
  =   
  if EventMap.mem e state.subscriptions_ then 
    let updsubs = delete u (EventMap.find e state.subscriptions_) in
    EventMap.add e updsubs state.subscriptions_ ;
  if UserMap.mem u state.notifications_ then 
    let updnotifs = delete e (UserMap.find u state.notifications_) in 
    UserMap.add u updnotifs state.notifications_ 

Both are correct with respect to the specification, which shows an example of a design choice made at implementation time.

The read action becomes trivial: it suffices to erase all elements in the notifications list of u, which can be done atomically.

  let read (u:user) 
    ensures  { read_spec u (old view state) (view state) } 
  =   
  UserMap.add u Nil state.notifications_

Finally, the occur function illustrates the practicality of being able to directly access the list of subscribers of a given event. **notify_users** is a helper function (see permalink for definition).

  let occur (e:event) : ()
    requires { EventMap.mem e state.subscriptions_ }
    ensures  { occur_spec e (old view state) (view state) } 
  =
  let users = EventMap.find e state.subscriptions_ in
  notify_users users e ;

Or alternatively (and defensively):

  let occur (e:event) : ()
    ensures  { occur_spec e (old view state) (view state) }
  =
  if EventMap.mem e state.subscriptions_ then
    let users = EventMap.find e state.subscriptions_ in
    notify_users users e ;

The complete example is available in the permalink.