Design Criteria

Replayability :

Accounting : archival

Archive :

Connections : labspace

Failure :

Collaboration : some hindsight at work.

Versions : labspace

Useability : labspace not inherently limited in Nuprl4.


Industry standards address some of the criteria.

Atomicity -

Consistency -

Isolation - serialiazability


Library Black Box

Old view of Library:

New view of library:


XA/DTP ORB Content/Application Servers

Consistent View - Isolation/Serializeability.

Distributed Cache/Directives/References.

Library Native Language / Dynamic Compilation.

Our Implementation - how we assure consistent view.

Directives :

lettype completion = (unit -> unit)
lettype directive = (unit -> (completion{undo} # completion{commit}))

an ordered list of uncompleted completions per transaction is maintained.

Atomicity :

it is an error to complete a completed completion.

If a transaction fails it implicitly undoes all pending completions.
If a transaction succeeds it implicitly commits all pending completions.

While it is possible to undo or commit pending completions during a transaction
it is not usually done.

Directives :

There are only six directives :

The library consists of a an association of abstract object ids with data.
This association is referred to as the library table.
The data is encapsulated in the primitive type object_contents.
We will see later the methods for creating object_contents.

lib_bind : object_id -> object_contents -> directive
lib_unbind : object_id -> directive

The library implements garbarge collection to remove unwanted objects from
the library table. Each object can be considered to have a sticky bit.
object_contents may contain concrete occurences of object_ids. Any object
which does not occur in the closure of concrete references of the sticky
objects are collectable.

lib_allow : object_id -> directive { sticky < - false, ie allow collection}
lib_disallow : object_id -> directive { sticky < - true }

root objects you see in the navigator.

There is also a bit to indicate liveness of an object.

lib_activate : object_id -> directive
lib_deactivate : object_id -> directive

Saving/Updating an object :

Deleting an object does not necessary

GC : unbind all objects not reachable from

For each directive there is an inverse.
Undo of directive == apply inverse.

Durability :

crash recovery : replay committed directives in journal

Serializability :

to gain write lock held by another.
abort -> no deadlock.

ObjectContents : not destructed

object_contents are non-destructive. Thus to modify
an object, you must instantiate a new object_contents
and then rebind the new contents to the object_id.

There are several object_contents modify functions which
follow the pattern
: object_contents -> *{data} -> object_contents.

kind : object_contents have a kind.

RULE INF{Inference} STM{Lemma} PRF{Proof}

TERM : kindless kind

term : object_contents have a term. For PRF contents the term is ignored.

properties : object_contents have an associated property list.
currently (tok # term) list, but will soon be extended to
((tok + object_id) # term) list.

Some kinds of object contents have extra data:
PRF : inference tree
STM : PRF list
INF : inference step

Evaluation :


enforces transaction scope.


objc_contents : tok{kind} -> object_contents
objc_kind : object_contents -> tok

objc_modify_source : object_contents -> term -> object_contents
objc_source : object_contents -> term

objc_get_properties : object_contents -> (tok # term) list
objc_set_properties : object_contents -> (tok # term) list

STM : source is statement of lemma.

stm_objc_modify_proofs : object_contents -> object_id list

stm_objc_proofs : object_contents -> object_id list

Inf Step : encapsulation of call to inference engine.

inf_step : term -> inf_step
inf_step_goal : inf_step -> term

inf_step_refine : term{desc} -> inf_step ->
term{tactic} -> term{context} -> inf_step

inf_step_refined_p : inf_step -> bool
inf_step_tactic : inf_step -> term
inf_step_subgoals : inf_step -> term list
inf_step_extract : inf_step -> term

INF : Source is Tactic.

inf_objc_modify_step : object_contents -> inf_step -> object_contents
inf_objc_delete_step : object_contents -> object_contents
inf_objc_step : object_contents -> inf_step

Inference Trees :

inf_tree : object_id{INF} -> inf_tree list -> inf_tree
inf_tree_object_id : inf_tree -> object_id
inf_tree_children : inf_tree -> inf_tree list


prf_objc_modify_inf_tree : object_contents -> inf_tree

prf_objc_delete_inf_tree : object_contents -> object_contents
prf_objc_inf_tree : object_contents -> inf_tree

OBJC API: Stamp, Reference, and Translation

Stamp : unique
by unique we mean if equal then they are the same stamp.

Translation :

Reference :

A reference is made when a lookup of the object_contents occurs.
For example, if a lemma is used in refining an inf_step, then
a reference to the lemma by the inf_step can be recorded. In
order to detect modifications to objects after a reference is
recorded, the stamp of the object_contents is noted in addition to
the object_id.

Consistency :

Onerus to require that there never be stale references.

Lack of read locks may result in stale references.

Certificates are a more general solution.

Distributed Cache API : Application Server

The distibuted cache handles the library broadcasts
and presents a consistent transaction view of the cached data to the

Objects are generally segregated in different table depending
on how the object data is broadcast by the library. The
library can be extended to broadcast new kinds of object data.
Objects must be ACTIVE to be distributed.

Table registry :

Application Server :

subscribe : object_id {table name} list

unsubscribe : object_id {table name} list -> unit
suspend : object_id {table name} list -> term {stamp}
resume : object_id {table name} list

< idle> : RECV req; < loop> < idle>
SEND req; < wait> < idle>
SEND note; < idle>
RECV note; < idle>

< wait> : RECV rsp
RECV note; < wait>
RECV req; < loop> < wait>

< loop> : SEND rsp
< send> < loop>

< send> : SEND note
SEND req; < wait>

Requests :
eval : term # term list -> unit
eval_to_term : term # term list -> term
send_notice : term -> unit


Callback : request form application to have application-server
call the application. Then application can send series of
requests and be sure they are all in same transaction.

Demand API :

Requires client to call application server each time a
object data is used. Due to the high bandwidth requirements,
this API will be used when an application server is available
in the client native language, thereby allowing compilation
of server into client.

We expect the client to supply hooks to implement table methods.

set_import_hook : object_id {table name} -> (term -> *) -> unit
set_match_hook : object_id {table name}

table_lookup : object_id {table name} -> object_id -> term
table_apply : object_id {table name} -> term -> term

In this API, the application server handles the account
of object dependencies. There is a hook to add references
besides those apparent from lookup and apply.

note_reference : tok -> object_id -> unit

limit_reference : object_id {table name}

only objects listed can be referenced.

Application Server Serial API :

The application server can present a serialized interface to
a client. The client and server interact via a single thread
of requests, notices, and responses.

< notice> : !add{kind}(< object-update> list)
!delete{kind}(< object-id> list)

< object-update> : !update{< object-id>:< o>}(< term>)

eagerly. The server is aware of (abstract ids) which objects
the client can reference, and thus need only push
those objects.

low-bandwidth, easier implementation

likely used when there is not an application server available
in client native language.


Reference Environment :

including listing of visible lemmas and abstractions.

Replayability provides testbed.

Pruned Marks theories to publish hybrid protocol.

Algebra replays


Working maps/Certificates.

True multi-threading