Skip to content

Instantly share code, notes, and snippets.

View peterson.csp
nametype t = 0..1
event P_begin, P_end
event Q_begin, Q_end
channel rd_flag0, wr_flag0 : t
channel rd_flag1, wr_flag1 : t
channel rd_turn, wr_turn : t
VAR(rd, wr, m) =
View m_prod_cons_cv_non_atomic_wait.c
#include "ddsv.h"
#define NUM_PROCESSES 2
#define MAX_COUNT 1
typedef unsigned prop_t; /* process id bit */
typedef struct shared_vars {
int mutex;
View subseq.thy
theory subseq imports "~~/src/HOL/Hoare/Hoare_Logic" begin
definition is_subseq :: "'a list => 'a list => bool" where
"is_subseq xs ys ==
(\<exists>c.
(\<forall>i. i + 1 < length ys --> c i < c (i + 1))
\<and> (length ys > 0 \<longrightarrow> c (length ys - 1) < length xs)
\<and> (\<forall>i. i < length ys \<longrightarrow> ys ! i = xs ! (c i)))"
fun is_subseq2 :: "'a list => 'a list => bool" where
View greedy_section.thy
(* Isabelle/HOL 2014 *)
theory "greedy_section" imports Main begin
definition sound :: "(nat * nat) set => bool" where
"sound X = (ALL p. p : X --> fst p < snd p)"
inductive_set greedy :: "(nat * nat) set => (nat * nat) list set"
for A :: "(nat * nat) set"
where
greedy_base:
View lim_a_n.thy
theory X imports Complex_Main begin
consts a :: "nat => real"
theorem
"k > 0 ==>
(ALL e. e > 0 --> (EX N1. (ALL n. n > N1 --> abs (a n - b) < e)))
= (ALL e. e > 0 --> (EX N2. (ALL n. n > N2 --> abs (a n - b) < k * e)))"
apply(rule iffI)
apply(rule allI)
View dominators.thy
theory Dominators imports Main begin
typedecl node
axiomatization
s0 :: "node" and
R :: "node rel"
where
reachable: "ALL n. (s0, n) : R^*"
View parallel-amb-callcc.scm
(use gauche.threads)
(define (amb . xs)
(call/cc
(lambda (k)
(if (null? xs)
((thread-specific (current-thread)) #f)
(begin
(for-each
(lambda (x)
View m_llsc.ml
open Ddsv
type shared_vars = {
x : int;
t1 : int;
t2 : int;
a1 : int;
a2 : int;
}
View m_cas.ml
open Ddsv
type shared_vars = {
m : int;
t1 : int;
t2 : int;
}
let show_sv r =
Printf.sprintf "m=%d t1=%d t2=%d" r.m r.t1 r.t2
View m_prod_cons_futex.ml
open Printf
open Ddsv
type shared_vars = {
mutex : int;
cv_bits : int;
cv_state : int;
cv_old : int list;
count : int;
}