Algebra

Design Criteria
Architecture/Specification
API
Status
Future

Replayability :

• confidence : can check.
  
• security : can check independently.
  
• testbed : Obvious.
  

Accounting : archival

• pruning
  
  • fine tuned export/inheritance
    
• allows coherency checks.
  
  • staleness : detect modification of referenced objects
    
• multiple explainations/organizations.
  

Archive :

• repository
  
  • reference algorithms
    
• share - publish -
  
  • merging separate development
    
• verification - replay
  
  • requires connect to application
    

Connections : labspace

• access clients to replay - execute certificates on remote clients.
  
  • record source of data.
    
• other refiners
  
• multiple refiners
  
• other editors
  
• access to lib from remote clients.
  

Failure :

• coarse : crash survivability.
  
  • labspace
    
• fine : avoid partial results if state modification fails.
  
  • archival
    

Collaboration : some hindsight at work.

• coarse - contributing.
  
  • archival
    
  • merge independent work.
    
  • merge related work
    
• fine
  
  • labspace
    
  • collegial : collaborative development
    
  • pedagogic : teacher can view during development.
    
  • administrative : can repair/upgrade while in use.
    

Versions : labspace

• Checkpoint
  
• Checkpoint object
  
  • liveness : convenient to be able to turn off
    
• without deleting.
  
• edit undo/redo
  

Useability : labspace not inherently limited in Nuprl4.

• browse
  
• search
  
• proof edit
  
  • lose subtree when modifying node.
    
  • limited/awkward cut/paste.
    
    • no proof cut buffers
      
  • avoid waiting during refinement.
    

ACID/DTP : OODBMS/XA

Industry standards address some of the criteria.

Atomicity -

• Failure:fine - avoid partial results if state modification fails.
  

Consistency -

• Accounting:pruning
  
• Accounting:coherency checks.
  

Isolation - serialiazability

• connections:
  
• concurrency
  
  • Collaboration:fine
    

Durability

• Falure:coarse - crash survivability
  
• Versions:checkpoints
  

Library Black Box

Old view of Library:


New view of library:

Distributed

• locally cached content.
  

XA/DTP ORB Content/Application Servers

Consistent View - Isolation/Serializeability.

Distributed Cache/Directives/References.
REQ/RSP/BROADCAST grammer.

• compilable-linkable application servers in application native language.
  

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 :

• commit : commits all prior commits as well.
  
• undo : undoes all later undos as well.
  

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 }

• there are generally only a handful of sticky objects. These are the
  

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

• object must be bound to be activated.
  
• object must be inactive to be unbound.
  

Saving/Updating an object :
deact/unbind/bind/act

Deleting an object does not necessary
deact

GC : unbind all objects not reachable from
disallowed.

• working map
  

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

Durability :

• directives are journaled as they are evaluated.
  
• At bind object_contents is written to disk.
  

crash recovery : replay committed directives in journal

Serializability :

• no read locks : choice not necessity.
  
• object write locks : abort if one transaction attempts
  

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.

• COM{Comment} TERM CODE DISP{Display}
  

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 :

ORB/XA

enforces transaction scope.

OBJC API :

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

• object_contents
  

STM : source is statement of lemma.

stm_objc_modify_proofs : object_contents -> object_id list

• object_contents
  

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

• desc identifies kind of inference engine.
  

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 :

prf_objc_modify_inf_tree : object_contents -> inf_tree

• object_contents
  

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 :

• expand library macros.
  
• validate object_contents (specific to object kind).
  
• stamps object_contents.
  
• object_contents must be translated for object to be active.
  

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 :

• can detect stale references.
  

Onerus to require that there never be stale references.

• replay makes staleness tolerable
  
• essential to be able to detect stale references.
  

Lack of read locks may result in stale references.

• equipped for stale references anyway.
  

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
application.

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 :

• object_id : name
  
• library methods :
  
  • export : object_contents -> term
    
  • filter : token {kind}
    
    • term {description}
      
    • object_id -> term{export} -> bool
      
  • ?maybe should supply objc instead of oid?
    

Application Server :

subscribe : object_id {table name} list

• term {description} -> unit
  

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

• term {stamp} -> unit
  

< 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

Response:
fail/value/ack

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.

• application server methods :
  
  • import : term -> *
    
  • match : term -> * -> bool
    
  • apply : term -> * -> term
    

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

• (term -> * -> bool) -> unit
  

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

• handles references
  
• high bandwidth.
  

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}

• object_id list -> unit
  

only objects listed can be referenced.

• may be easier to check in cache than by application itself.
  

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

• note that there is not a requirement that push be done
  

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.

Status

Reference Environment :

• encapsulation of tactic reference variable bindings
  

including listing of visible lemmas and abstractions.

• approximation to stable code.
  

Replayability provides testbed.

• Mark's Obvious tactic
  

Pruned Marks theories to publish hybrid protocol.

• example of working lib -> archive lib
  

Algebra replays

PVS/MetaPrl

Working maps/Certificates.

True multi-threading