逐次一貫性下の知識伝達を表す
直観主義様相論理
Yoichi Hirai

2010-03-03

Overview
Contribution 0: intuitionistic epistemic logic
deduction system, semantics.
soundness, strong completeness, disjunction property, finite model
property, decidability.
Contribution 1: formalising sequential consistency
Sequential consistency as pKm ϕ  Km ψ q _ pKm ψ  Km ϕq.
Unexpected application of an intermediate logic.
Contribution 2: decidable abstraction of waitfreely solvable tasks

Is a task waitfreely solvable or not?
Original task: undecidable
Abstract task: decidable

Contribution 1: Formalising Sequential Consistency

Contribution 2: Decidable abstraction of waitfreely
solvable tasks

Contribution 2: Decidable abstraction of waitfreely
solvable tasks

Contribution 0

Intuitionistic Epistemic Logic

New informal reading of Kp ϕ
Formula ϕ :: K | I | ϕ ^ ϕ | ϕ _ ϕ | ϕ  ϕ | Kp ϕ.
Same as classical epistemic logic [Hintikka, 1962].

Kp ϕ: p knows ϕ. (What does “know” mean?)Classical In all p’s possible worlds, ϕ is true.
This workp has received a proof of ϕ.

c.f. justified, true belief as in Plato: Theaetetus.

New informal reading of Kq Kp ϕ: COMMUNICATIONKq Kp ϕ: q knows that p knows ϕ.
Classical In all q’s possible worlds, in all p’s possible worlds,
ϕ is true.
This work q has received a proof of the fact thatp has received a proof of ϕ.
Communication from p to qFormal Semantics = Intuitionistic Logic (+ Knowledge)
model xW , ¨, pfp qpPA yfp : W Ñ W : idempotent, descending, monotonic

valuation ρ : PVar Ñ P pW q

ρpI q: downward-closedDefine w |ù ϕ for a state w P W and a formula ϕ:w |ù Kw |ù I

w |ù Kp ψw |ù ψ0 ^ ψ1w |ù ψ0 _ ψ1w |ù ψ0  ψ1

ô neverô w P ρp I q
ô fp pw q |ù ψô both w |ù ψ0 and w |ù ψ1 hold
ô either w |ù ψ0 or w |ù ψ1 holds
ô v |ù ψ0 implies v |ù ψ1 for any v © w .

Formal Semantics = Intuitionistic Logic (+ Knowledge)
model xW , ¨, pfp qpPA y
fp : W Ñ W : idempotent, descending, monotonicpast¨futureFormal Semantics = Intuitionistic Logic (+ Knowledge)
model xW , ¨, pfp qpPA y
fp : W Ñ W : idempotent, descending, monotonicpast¨

futureFormal Semantics = Intuitionistic Logic (+ Knowledge)
model xW , ¨, pfp qpPA y
fp : W Ñ W : idempotent, descending, monotonicpast¨

futureFormal Semantics = Intuitionistic Logic (+ Knowledge)
model xW , ¨, pfp qpPA y
fp : W Ñ W : idempotent, descending, monotonicpast¨

futureFormal Semantics = Intuitionistic Logic (+ Knowledge)
model xW , ¨, pfp qpPA y
fp : W Ñ W : idempotent, descending, monotonic
pastp’s state.

¨futureFormal Semantics = Intuitionistic Logic (+ Knowledge)
model xW , ¨, pfp qpPA y
fp : W Ñ W : idempotent, descending, monotonic
past
p’s state. q’s state.

¨futureDeduction SystemΓ $ Kp ϕ
Γ$ϕ(T)(necessitation)(ax)$ϕϕ(introspection)
Γ$ϕ
Kp Γ $ Kp ϕ(w)

Γ$ψ
$ϕψ

ϕ, ΓΓ

1ϕ, ϕ, ΓΓ$ ψ0 _ ψ1Γ( -E)Γ$ϕ$ϕΓ, ψ0$ ψ0  ψ1
Γ $ ψ1Γ, ψ1Γ

$ϕ$ϕΓ$ϕ^ψ(^-E1 )
Γ$ψ
Γ$ϕ(_-I1 )
Γ$ψ_ϕ(e)

1ϕ, Γ

1_

(c)

1

Γ

( -E)

( -I)

Γ $ Kp pϕ _ ψ q
Γ $ Kp ϕ _ Kp ψ$ϕ$ϕ
Γ$ϕ
Γ $ψ
(^-I)
Γ, Γ $ ϕ ^ ψ$ϕ$ϕ

ψ, Γ$ϕ^ψ
Γ$ϕΓ$ϕ(_-I0 )
Γ$ϕ_ψ^

( -E0 )

(_K )

$ ψ0

Γ $ Kp ϕΓ $ Kp Kp ϕ$ϕ

Γ, ϕ, ψ, Γ1

1

Γ, ψ, ϕ, Γ1

1K

( -E)

ΓΓ

$K$ϕ

Theoretical Results
Soundness and strong completeness Γ |ù ϕ
Disjunction property $ ϕ _ ψ ùñby extending Aczel’s slash relation.

ðñΓ $ ϕ.

$ ϕ or $ ψ(revising, seeking for more general approach.)Defining fp pΓq: agent p’s view on a set of formulas Γ.
gp pΓq  tϕ P Fml | pKp q ϕ P Γ and ϕ does not begin with Kp u,
fp pΓq  gp pΓq Y Kp gp pΓq Y tϕ P Fml | Γ $ Ku.

Finite model property M |ù ϕ for all finite M ðñ M |ù ϕ for all M
by modifying subformula relation in [Sato, 1977]
Decidability It is decidable whether $ ϕ.

Contribution 1

Modelling Sequential Consistency

Need for shared memory consistency
Assumption: full-information
 A message contains all knowledge of its sender.
 Nothing is ever forgotten.

Even under this assumption, no communication is guaranteed
between processes.

Essence of Sequential Consistency
For two memory states, either ¨ or © holds.

Essence of Sequential Consistency
For two memory states, either ¨ or © holds.

Logical Background: logic Lin for linear models
Lin  Intuitionistic logic pϕ  ψ q _ pψ  ϕq:
Intuitionistic logic  Lin  Classical logic

Well-known property:
Lin $ θ ðñ M |ù θ for all linear model M(Linear model: for any two states, either ¨ or © holds.)

A logic SC for Sequential Consistency
SC  Int. Epistemic logic pKm ϕ  Km ψ q _ pKm ψ  Km ϕq:
Intuitionistic epistemic logic  SC  Classical logic

A result:

SC $ θ ðñ M |ù θ for all sequential model M(Sequential model: for any two memory states, ¨ or © holds.)

An example theorem under sequential consistency$ ppKp Km Kp I q ^ Kq Km Kq J q  ppKq Kp I q _ Kp Kq J qInformal reading p sends a proof of I to m, then m replies to p.
 q sends a proof of J to m, then m replies to q.
 then, p’s knowledge has been transmitted to q,or q’s knowledge has been transmitted to p.
A proof of this contains 55 steps (cf. it was 1 step).

Ongoing work: finite model property of SC
Trying to avoid
logically possible but computationally impossible schedules like
infinitehkkkkkkkkkkkkkkikkkkkkkkkkkkkkj
t0 ¬ t1 ¬ t2 ¬    tn . . . ¬ t 1Status
1. Find a proof strategy.
2. A gap found. Fix or abort.

3. No gaps found. Write and revise until find one. Ð current

Contribution 2

Decidable Abstraction of Waitfreely
Solvable Tasks

Waitfree Computation
Sequential consistency: restriction on schedules.
Waitfreedom: restriction on programs.
Informal meaning
No process waits for another process.
Formal meaning k exists
each process accesses the shared memory at most k times
in any scheduling.

Undecidability and decidability
It is undecidable whether a task is waitfreely solvable[Gafni and Koutsoupias, 1999].
task: a set of allowed (input values, output values) pairs.
It is decidable whether a communication is waitfreely attainable(new)
Waitfree task description ψ is defined with the BNF:ψ :: Kp ψ | ψ ^ ψ | ψ _ ψ | Ip
where a proof of Ip represents initial knowledge of p.
yes pKq Kp Ip q _ Kp Kq Iq
no pKq Kp Ip q ^ Kp Kq Iq

Future Work
Extending program extraction to concurrent/distributedcomputation.
 Modelling other memory consistencies: especially

PRAM consistency, cache consistency and processor
consistency
 typed lambda calculusFor multi-core?
Type-safe Paxos [Lamport, 1997] implimentation

 Quantify agents
DxKx ϕ for program extraction with mobility.

Knowledge of π-calculus terms?

 Knowledge of forking and merging agents

This work has been accepted to LPAR-16 held in Dakar, Senegal.

Gafni, E. and Koutsoupias, E. (1999).
Three-processor tasks are undecidable.
SIAM Journal on Computing, 28(3):970–983.
Hintikka, J. (1962).
Knowledge and belief: an introduction to the logic of the two notions.
Cornell University Press.
Lamport, L. (1997).
How to make a correct multiprocess program execute correctly on a multiprocessor.
IEEE Transactions on Computers, 46(7):779–782.
Sato, M. (1977).
A study of Kripke-type models for some modal logics by Gentzen’s sequential method.
Publications of the research institute for mathematical sciences, 13:381.