In the previous post, we talked about snapshots. However, we did not give the rigor for the correctness of the marker approach. In the current post, I want to show just that. The snapshot is the accurate picture of the global state.
The goal here is to make sure that each computation occurred. We do this by labeling each action in the computation as either pre or post. This helps us know which actions occured before the local state was saved and which actions occurred after the state was saved. A pre action is the action that was recorded before the local state was saved. And the post action is the action that was taken after the state was saved. The actual computation occurred with a interleaved sequence of pre and post actions. We will swap adjacent pre and post actions in the computation. We will retain the order of all the pre's as they appear in the original. We will also retain the order of all the post's as they appear in the original. This way we have ordered all the pres to occur before the state was saved and all the posts to occur after the state was saved. By swapping and retaining the order, we want to have an equivalent computation as the original where each computation can be acertained to have occurred.
To complete the equivalency, let us look at the swapping of a pair of actions that are out of order. Such a pair has the form <apost, bpre>. The a and b are different processes.
There are three cases for bpre:
bpre is a local action. In this case, local actions can be swapped since the two does not affect each other.
bpre is a send action. In this case too the swap can be done.
bpre is a receive action. The only case we cannot swap with apost is when apost is the corresponding send. We show that it is impossible for apost to be a corresponding send because the markers must have been sent and since the channels are a queue, the marker must be delivered before the message sent in action a. So b must be a post and they cannot be out of order.
Thus in all cases we are able to swap. By continuing with the swapping until the desired sequence of all pres and all posts, we establish equivalency and the correctness that the snapshot is accurately taken by the markers approach.
The goal here is to make sure that each computation occurred. We do this by labeling each action in the computation as either pre or post. This helps us know which actions occured before the local state was saved and which actions occurred after the state was saved. A pre action is the action that was recorded before the local state was saved. And the post action is the action that was taken after the state was saved. The actual computation occurred with a interleaved sequence of pre and post actions. We will swap adjacent pre and post actions in the computation. We will retain the order of all the pre's as they appear in the original. We will also retain the order of all the post's as they appear in the original. This way we have ordered all the pres to occur before the state was saved and all the posts to occur after the state was saved. By swapping and retaining the order, we want to have an equivalent computation as the original where each computation can be acertained to have occurred.
To complete the equivalency, let us look at the swapping of a pair of actions that are out of order. Such a pair has the form <apost, bpre>. The a and b are different processes.
There are three cases for bpre:
bpre is a local action. In this case, local actions can be swapped since the two does not affect each other.
bpre is a send action. In this case too the swap can be done.
bpre is a receive action. The only case we cannot swap with apost is when apost is the corresponding send. We show that it is impossible for apost to be a corresponding send because the markers must have been sent and since the channels are a queue, the marker must be delivered before the message sent in action a. So b must be a post and they cannot be out of order.
Thus in all cases we are able to swap. By continuing with the swapping until the desired sequence of all pres and all posts, we establish equivalency and the correctness that the snapshot is accurately taken by the markers approach.
No comments:
Post a Comment