proposition: Lemma LockServ_mutual_exclusion_trace : forall st tr, step_async_star step_async_init st tr -> trace_mutual_exclusion tr /\ (forall n, last_holder tr = Some n -> held (nwState st (Client n)) = true) /\ (forall n, held (nwState st (Client n)) = true -> last_holder tr = Some n).
proof: Proof. Proof using. apply cross_relation; intros. - intuition. + red. red. auto. + unfold last_holder in *. simpl in *. discriminate. + unfold last_holder in *. simpl in *. discriminate. - match goal with | [ H : step_async _ _ _ |- _ ] => invcs H end; monad_unfold; repeat break_let; repeat find_inversion. + unfold NetHandler in *. break_match. * find_apply_lem_hyp ClientNetHandler_cases. break_and. { break_or_hyp. - intuition; subst. + apply trace_mutex'_no_out_extend; auto. + rewrite update_nop_ext. find_apply_lem_hyp last_holder'_no_out_inv. auto. + match goal with | [ H : _ |- _ ] => rewrite update_nop in H end. find_apply_hyp_hyp. apply last_holder'_no_out_extend. auto. - intuition; subst. + apply trace_mutex'_locked_extend. auto. destruct (last_holder' None tr) eqn:?; auto. find_apply_hyp_hyp. erewrite locked_in_flight_all_clients_false in * by eauto using locks_correct_locked_invariant, reachable_intro, locks_correct_invariant. discriminate. + my_update_destruct; try find_inversion; rewrite_update; auto. find_apply_lem_hyp last_holder'_locked_some_eq. congruence. + my_update_destruct; try find_inversion; rewrite_update. * apply last_holder'_locked_extend. * erewrite locked_in_flight_all_clients_false in * by eauto using locks_correct_locked_invariant, reachable_intro, locks_correct_invariant. discriminate. } * { find_apply_lem_hyp ServerNetHandler_cases. break_and. subst. repeat split. - apply trace_mutex'_no_out_extend. auto. - intros. my_update_destruct; try discriminate. rewrite_update. find_apply_lem_hyp last_holder'_no_out_inv. auto. - intros. my_update_destruct; try discriminate; rewrite_update. apply last_holder'_no_out_extend. auto. } + unfold InputHandler in *. break_match. * unfold ClientIOHandler in *. { monad_unfold. repeat break_match; repeat find_inversion; intuition; repeat rewrite snoc_assoc in *; try apply trace_mutex'_no_out_extend; try find_apply_lem_hyp last_holder'_no_out_inv; try (apply last_holder'_no_out_extend; auto). - apply trace_mutual_exclusion'_extend_input; auto. congruence. - rewrite update_nop_ext. find_apply_lem_hyp last_holder'_input_inv; try congruence. auto. - match goal with | [ H : _ |- _ ] => rewrite update_nop in H end. apply last_holder'_input_extend; auto. congruence. - apply trace_mutex'_unlock_extend; auto. - rewrite last_holder_unlock_none in *; auto. discriminate. - my_update_destruct; try find_inversion; rewrite_update. + discriminate. + assert (mutual_exclusion (nwState st)) by eauto using mutual_exclusion_invariant, reachable_intro. unfold mutual_exclusion in *. assert (c = n) by eauto. congruence. - apply trace_mutex'_unlock_extend. auto. - rewrite update_nop. find_apply_lem_hyp last_holder_some_unlock_inv. auto. - match goal with | [ H : _ |- _ ] => rewrite update_nop in H end. assert (n <> c) by congruence. find_apply_hyp_hyp. apply last_holder'_neq_unlock_extend; auto. - apply trace_mutual_exclusion'_extend_input; auto. congruence. - rewrite update_nop_ext. find_apply_lem_hyp last_holder'_input_inv; try congruence. auto. - match goal with | [ H : _ |- _ ] => rewrite update_nop in H end. apply last_holder'_input_extend; auto. congruence. } * unfold ServerIOHandler in *. monad_unfold. find_inversion. { intuition; repeat rewrite snoc_assoc in *. - apply trace_mutex'_no_out_extend. apply trace_mutual_exclusion'_extend_input_server. auto. - find_apply_lem_hyp last_holder'_no_out_inv. rewrite update_nop. find_apply_lem_hyp last_holder'_input_inv_server. auto. - apply last_holder'_no_out_extend; auto. rewrite_update. unfold last_holder. rewrite last_holder'_server_extend. auto. } Qed.
imports: Verdi(Verdi HandlerMonad) StructTact(Fin) Verdi(StatePacketPacketDecomposition)