
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  %  This module augments the basic CTR interpreter with  %
  %  procedures for durable and recoverbale execution.    %
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


:- export start/1, continue/0, request/1, logWrite/1.

:- import reverse/2 from basics.
:- import oneStep/3 from 'ctr.pl'.
:- import ins/1, del/1 from 'updates.pl'.
:- import file_write/2 from xsb_writ.
:- import file_read/2 from xsb_read.
:- import file_open/3, file_close/1, file_flush/2, file_seek/4,
          file_pos/2, file_truncate/3 from file_io.


% USER INTERFACE: To execute a goal, the user types "start(Goal)".
% If the system crashes during execution, the user can resume
% execution from the last checkpoint.  To do this, he must first
% restart the ctr interpreter with the same transaction base and the
% original database.  He must then type "continue", which restores
% the database and the goal to their states as of the last
% checkpoint before the crash.  Execution then resumes from that
% point.  
%
% CHECKPOINTS and TRANSACTIONS : A CTR program is executed as a
% sequence of transactions (called "hot components" in the proof
% theory).  Checkpoints are carried out between these transactions.
% Checkpoints are requested from a CTR program by the command
% "request(checkpoint)", and are carried out as soon as the current
% transaction is finished.
%
% BACKTRACKING and ROLLBACK: there is no backtracking or rollback
% at the top level (i.e., outside all transactions), where
% deadlock is interpreted as "wait".  Backtracking and rollback
% occur only inside transactions, where deadlock is interpreted as
% "abort".  One consequence is that backtracking only occurs between
% checkpoints.  Thus, the checkpoint mechanism does not need to save
% any backtracking information.
%
% THE INTERPRETER: Execution at the top-level is handled by the code
% in this file, which implements checkpoints and recovery, and which
% maintains several disk-based logs.  This code invokes the basic CTR
% interpreter (which supports backtracking and rollback) to execute
% individual transactions.  The predicates start/1 and continue/0 are
% the basic interface to the top-level interpreter.

start(Goal) :- beginLog(Goal), executeD(Goal).

continue :- recover(Goal), executeD(Goal).


% THE BASIC INTERPRETIVE LOOP: The predicate executeD/1 executes a
% goal (durably) by repeatedly executing hot components (or "steps")
% until the empty goal is reached.  Unlike the basic CTR interpreter
% (which uses recursion to simulate iteration), the rule below uses an
% explicit "repeat" construct.  This allows the execution of a goal to
% continue indefinitely without generating a huge subroutine stack.
% In general, the repeat construct forces the following statement to
% execute repeatedly until it no longer fails.  In this case, it
% forces the predicate oneStepD/0 to execute repeatedly until
% goal(state) is true.  A cleanup procedure is then called, and
% execution terminates.  During the execution, the goal is stored in
% the database in the predicate goal/1, and each iteration of the
% repeat statement reads and updates the goal (via the predicate
% oneStepD/0).

executeD(Goal) :- initialize(Goal),
                  repeat,
                    (goal(state) -> cleanup; oneStepD, fail).



% The predicate initialize/1 clears all requests from the database,
% removes any earlier goals, and stores the current goal.

initialize(Goal) :- retractall(req(_)),
                    retractall(goal(_)),
                    assert(goal(Goal)).


% When the goal has finished executing, the predicate cleanup/0
% carries out a final checkpoint operation, and then closes all the
% logs.

cleanup :- checkpoint(state), endLog.


% ONE-STEP EXECUTION: The predicate oneStepD/0 executes one hot
% component (or step) of the current goal.  The step is executed as a
% transaction by invoking the predicate oneStep/3 from the basic CTR
% interpreter.  During execution, all the updates invoked by the step
% are recorded (temporarily) in a main-memory log.  After execution,
% this record is transferred to a disk-based log (by the predicate
% transferLog/0).  In addition, if the step generated a request for a
% checkpoint, then the checkpoint is carried out (by the predicate
% checkpoint/1).  Finally, the state of the goal is updated.

oneStepD :- goal(Goal1),
            oneStep(all,Goal1,Goal2),
            transferLog,
            (req(checkpoint) -> checkpoint(Goal2),
                                retractall(req(checkpoint)); true),
            retractall(goal(Goal1)),
            assert(goal(Goal2)),
            !.


% REQUESTING CHECKPOINTS: The predicate request/1 is part of the
% interface to the recoverable CTR interpreter.  This predicate is
% used inside a CTR program to request a service, S, from the
% interpreter.  The predicate request/1 simply stores the request in
% the database, for servicing by the CTR interpreter at a later time.
% At present, checkpoints are the only service supported by the
% interpreter.

request(S) :- assert(req(S)).



% LOGS: To recover from system crashes, the interpreter maintains
% three logs, each stored in a file on disk.  The file "log.updates"
% records every update and checkpoint executed by the program.  This
% log is used to implement roll-forward recovery of the Prolog
% database after a system crash.  The files "log.goal1" and
% "log.goal2" record the current and previous goals (i.e., the program
% state).  These two files are used to restore the goal after a system
% crash.  Unlike the update log, which stores a sequence of small
% atoms, the goal logs each store a single large atom.  In the update
% log, new atoms are simply appended to the end of the file.  However,
% in the goal logs, each new atom overwites the previous one.  This is
% why two goal logs are needed: if the systems crashes while the
% current goal is being written to one goal log (which often happens),
% then the previous goal can still be recovered from the other goal
% log.  During execution, the logging of goals toggles back and forth
% between the files log.goal1 and log.goal2.
%
% In addition to the disk-based logs described above, the interpreter
% maintains a small log in main memory.  This log records the sequence
% of committed updates performed by the current top-level transaction.
% The log is stored in the XSB database in the predicate updates(L),
% where L is a list of updates.  This list acts as a stack: updates are
% pushed onto L during transaction execution, and popped off of L during
% backtracking.  If the transaction aborts, then L will end up empty.
% However, if the transaction commits, then L will contain the sequence
% of committed updates performed by the transaction.  These updates are
% written to the disk-based log in the file "updates.log".  L is then
% reinitialized to the empty list at the beginning of each new top-level
% transaction.  Assuming that the transactions are short, we expect L to
% be short, and to easily fit in main memory.
%
% The predicate beginLog/1 initializes the logs.  It opens the three
% files, stores the current goal in one of them (log.goal1), stores the
% file descriptors in the Prolog database, and then initializes the
% main-memory (MM) log to the empty list.

beginLog(Goal) :- file_open('log.updates', 1, FileUp),   % Open for writing.
                  file_open('log.goal1', 1, FileG1),     % Open for writing.
                  file_open('log.goal2', 1, FileG2),     % Open for writing.
                  writeAtom(Goal,FileG1),
                  assert(updateLog(FileUp)),        % Store file descriptor.
                  assert(goalLogs(FileG1,FileG2)),  % Store file descripors.
                  assert(updates([])).              % Initialize the MM log.


% When a CTR program has finished executing, the predicate endLog/0
% closes all the log files.

endLog :- updateLog(FileUp),
          goalLogs(FileG1,FileG2),
          file_close(FileUp),
          file_close(FileG1),
          file_close(FileG2).


% EXECUTING CHECKPOINTS: The predicate checkpoint/1 carries out
% a checkpoint operation.  Note that the last action is to write
% the atom "checkpoint" to the update log, and flush the log to
% disk.  Thus, if the atom "checkpoint" appears in the log, then
% we know that a crash did not occur before the checkpoint
% operation completed.  (This fact is used during recovery.)

checkpoint(Goal) :-               %%% THE GOAL LOGS:
     goalLogs(FileG1,FileG2),       % Retrieve the two goal logs.
     file_truncate(FileG2,0,_),     % Erase the first goal log.
     writeAtom(Goal,FileG2),        % Write the current goal.
     file_flush(FileG2,_),          % Flush the goal log.
     swapFiles(FileG1,FileG2),      % Swap the two goal logs.
                                  %%% THE UPDATE LOG:
     updateLog(FileUp),             % Retrieve the update log.
     writeAtom(checkpoint,FileUp),  % Write 'checkpoint' to update log.
     file_flush(FileUp,_).          % Flush the update log.


% The predicate swapFiles/2 reverses the order of the file
% descriptors for the two goal logs, as stored in the database.

swapFiles(FileG1,FileG2) :- retract(goalLogs(FileG1,FileG2)),
                            assert(goalLogs(FileG2,FileG1)).



% LOGGING UPDATES: The predicate logWrite/1 appends an update to the
% main-memory log.  During backtracking, the predicate onBacktracking/1
% removes the update from the log.  Recall that this log is stored in
% the XSB database in the atom updates(L), where L is a list of updates.
% The predicate logWrite/1 is invoked whenever a CTR program attempts to
% update the Prolog database.  Note: if the recovery module is not being
% used (in which case logging is not needed), then the predicate
% logWrite/1 has no effect.

logWrite(Update) :-
     updates(List) -> retractall(updates(_)),
                      assert(updates([Update|List])), !,
                      onBacktracking(List);
                      true.

onBacktracking(List).

onBacktracking(List) :- retractall(updates(_)),
                        assert(updates(List)), !,
                        fail.


% The predicate transferLog/1 transfers the contents of the main-memory
% update log to the disk-based update log, and then resets the
% main-memory (MM) log to be empty.  This predicate is invoked each time
% a top-level transaction completes.

transferLog :- updates(List1),            % Get update list from MM log.
               reverse(List1,List2),
               updateLog(File),           % Get file descriptor of disk log.
               writeAtoms(List2,File),    % Write updates to disk log.
               retractall(updates(_)),    % Reset MM log to be empty.
               assert(updates([])).


% Given a list of atoms and a file descriptor,
% the predicate writeAtoms/2 writes each atom to the file.
%
writeAtoms([Atom|List], File) :- writeAtom(Atom,File),
                                 writeAtoms(List,File).

writeAtoms([],File).


% Given an atom and a file descriptor, the predicate writeAtom/2
% appends the atom to the end of the file, followed by a period and an
% end-of-line character.
%
writeAtom(Atom,File) :-
           file_write(File,Atom),
           file_write(File,'.
').



% RECOVERY:
% After a system crash, the predicate recover/1 restores the
% database, the logs, and the goal to the state they had as of the
% last checkpoint before the crash.  The restored goal is returned.
%
% Recovery takes place in two stages: first, the database and the
% logs are restored to their state as of the last checkoint; then,
% the logs are reopenned and the goal is restored.  The variable
% GoalLogs is an ordered pair containing the names of the two goal
% logs, where the first log in the pair stores the goal as of the
% last checkpoint.  The goal is restored from this first log.

recover(Goal) :- restore(GoalLogs), reopenLogs(GoalLogs,Goal).


% The predicate restore/1 restores the database and the update log
% to their state as of the last checkpoint.  It also returns the
% names of the goal logs (as an ordered pair), as described above.
% To restore the update log, a new copy of the log is created in
% which all entries after the last checkpoint are removed (since
% execution, including logging, will resume from the last
% checkpoint).  Most of the actual work is done by the predicate
% rollforward/4, while the job of restore/1 is to open, close and
% rename the appropriate files.  Note that the old update log is
% moved to the file "log.updates.old".  If the system crashes
% during recovery, then "log.updates.old" should be moved back to
% "log.updates", and the entire recovery process should be started
% from scratch.  All files are closed when restore/1 returns.

restore(GoalLogs2) :-
    unix('mv log.updates log.updates.old'),
    file_open('log.updates', 1, NewLog),             % Open for writing.
    file_open('log.updates.old', 0, OldLog),         % Open for reading.
    GoalLogs1 = ['log.goal1','log.goal2'],
    rollForward(NewLog,OldLog,GoalLogs1,GoalLogs2),
    file_close(NewLog),
    file_close(OldLog).


% The predicate reopenLogs/2 reopens the logs, stores their file
% descriptors in the Prolog database, and restores the goal.  The
% variables LogG1 and LogG2 provide the names of the two goal logs.
% The goal itself is restored from LogG1, and is returned as the
% value of the variable Goal.  Note that LogG1 is openned for
% reading, then closed, then reopenned for writing.

reopenLogs([LogG1,LogG2],Goal) :-
    file_open(LogG1,0,Descr),             % Open for reading.
    file_read(Descr,Goal),                % Restore the goal.
    file_close(Descr),
    file_open('log.updates', 2, FileUp),
    file_open(LogG1,1,DescrG1),           % Open for writing.
    file_open(LogG2,1,DescrG2),           % Open for writing.
    writeAtom(Goal,DescrG1),
    assert(updateLog(FileUp)),            % Store file descriptor.
    assert(goalLogs(DescrG1,DescrG2)),    % Store file descriptors.
    assert(updates([])).               % Store an empty update list.



% ROLLING FORWARD THE LOG:
% The predicate rollforward/4 restores the database and the
% update log while scanning the old update log.  It also determines
% from which goal log the goal should be restored.  It is a
% recursive predicate with one level of recursion for each
% checkpoint in the update log.  At each recursive call, it first
% searches for the next checkpoint.  If none is found, it simply
% terminates.  If one is found, then it executes every update in
% the log from the current position in the log up to the next
% checkpoint in the log.  It then swaps the two goal logs, and
% calls itself recursively.
%
% NewLog is the file descriptor for the new (initially empty)
% update log.  Old Log is the file descriptor for the old update
% log.  GoalLogs1 is an ordered pair containing the names of the
% two goal logs.  The order of the names in this pair is reversed
% (swapped) each time a checkpoint is read.  The final value of
% GoalLogs1 (after the old update log has been completely
% scanned) is returned as GoalLogs3.  Consequently, the first
% element of GoalLogs3 is the name of the log from which the goal
% is to be restored.

rollForward(NewLog,OldLog,GoalLogs1,GoalLogs3) :-
       file_pos(OldLog,Pos),           % Note position in old update log.
       findCheckpoint(OldLog), !,      % Find next checkpoint.
       file_seek(OldLog,Pos,0,_),      % Return to noted position.
       execUpdates(NewLog,OldLog),     % Execute updates stored in the log.
       swapLogs(GoalLogs1,GoalLogs2),  % Change the order of the goal logs.
       rollForward(NewLog,OldLog,GoalLogs2,GoalLogs3).


% When this rule is reached, there are no more checkpoints left,
% and the old update log has been completely scanned.  At this
% point, the value of GoalLogs1 is simply returned as GoalLogs3.
%
rollForward(NewLog,OldLog,GoalLogs,GoalLogs).


% Swap the elements of an ordered pair.
%
swapLogs([X,Y],[Y,X]).


% Starting from the current position in the old update log, the
% predicate findCheckpoint/1 scans forward through the log
% searching for the next checkpoint.  If one is found, then the
% predicate succeeds.  If one is not found (i.e., if an end-of-file
% is found first), then the predicate fails.

findCheckpoint(OldLog) :-
       file_read(OldLog,Atom),
       not(Atom = end_of_file),
       (Atom = checkpoint -> true; findCheckpoint(OldLog)).


% Starting from the current position in the old update log, the
% predicate execUpdates/2 scans forward through the log searching
% for the next checkpoint.  In the process, it executes each update
% command that it finds, and copies it to the new update log.
% execUpdates/2 assumes that a checkpoint will eventually be
% found.

execUpdates(NewLog,OldLog) :- file_read(OldLog,Atom),
                              writeAtom(Atom,NewLog),
                              exec1(Atom),
                              (Atom = checkpoint ->
                                 true; execUpdates(NewLog,OldLog)).


exec1(ins(P)) :- !, ins(P).   % Execute a database insert.
exec1(del(P)) :- !, del(P).   % Execute a database delete.
exec1(P).                     % Ignore any other commands.



% Declare to the XSB system that predicate P exists.
%
declarePred(P) :- assert(P), retract(P).

 :- declarePred(req(dummy)).
 :- declarePred(updateLog(dummy)).
 :- declarePred(goalLogs(dummy)).
 :- declarePred(updates(dummy)).
