Skip to main content

telltale_runtime/compiler/
analysis.rs

1// Static analysis for choreographic protocols
2
3use crate::ast::{Choreography, Protocol, Role};
4use std::collections::{HashMap, HashSet};
5
6#[path = "analysis_graph.rs"]
7mod analysis_graph;
8use analysis_graph::{has_communication, has_cycle};
9
10/// Analysis results for a choreography
11#[derive(Debug)]
12pub struct AnalysisResult {
13    pub is_deadlock_free: bool,
14    pub has_progress: bool,
15    pub role_participation: HashMap<Role, ParticipationInfo>,
16    pub warnings: Vec<AnalysisWarning>,
17    pub communication_graph: CommunicationGraph,
18}
19
20/// Information about a role's participation
21#[derive(Debug)]
22pub struct ParticipationInfo {
23    pub sends: usize,
24    pub receives: usize,
25    pub choices: usize,
26    pub is_active: bool,
27}
28
29/// Warning generated during analysis
30#[derive(Debug, Clone)]
31pub enum AnalysisWarning {
32    UnusedRole(Role),
33    PotentialDeadlock(String),
34    NoProgress(String),
35    AsymmetricChoice(Role),
36    UnreachableCode(String),
37}
38
39/// Communication graph for visualization
40#[derive(Debug, Clone)]
41pub struct CommunicationGraph {
42    pub nodes: Vec<Role>,
43    pub edges: Vec<(Role, Role, String)>, // (from, to, message)
44}
45
46/// Analyze a choreography for correctness properties
47#[must_use]
48pub fn analyze(choreography: &Choreography) -> AnalysisResult {
49    let mut analyzer = Analyzer::new(choreography);
50    analyzer.analyze()
51}
52
53struct Analyzer<'a> {
54    choreography: &'a Choreography,
55    warnings: Vec<AnalysisWarning>,
56    role_stats: HashMap<Role, RoleStats>,
57    comm_graph: CommunicationGraph,
58}
59
60#[derive(Default)]
61struct RoleStats {
62    sends: usize,
63    receives: usize,
64    choices: usize,
65}
66
67impl<'a> Analyzer<'a> {
68    fn new(choreography: &'a Choreography) -> Self {
69        let mut role_stats = HashMap::new();
70        for role in &choreography.roles {
71            role_stats.insert(role.clone(), RoleStats::default());
72        }
73
74        Analyzer {
75            choreography,
76            warnings: Vec::new(),
77            role_stats,
78            comm_graph: CommunicationGraph {
79                nodes: choreography.roles.clone(),
80                edges: Vec::new(),
81            },
82        }
83    }
84
85    fn analyze(&mut self) -> AnalysisResult {
86        // Collect statistics
87        self.analyze_protocol(&self.choreography.protocol);
88
89        // Check for deadlocks
90        let is_deadlock_free = self.check_deadlock_freedom();
91
92        // Check for progress
93        let has_progress = self.check_progress();
94
95        // Check role participation
96        let role_participation = self.compute_participation_info();
97
98        // Check for unused roles
99        for role in &self.choreography.roles {
100            if let Some(info) = role_participation.get(role) {
101                if !info.is_active {
102                    self.warnings
103                        .push(AnalysisWarning::UnusedRole(role.clone()));
104                }
105            }
106        }
107
108        AnalysisResult {
109            is_deadlock_free,
110            has_progress,
111            role_participation,
112            warnings: self.warnings.clone(),
113            communication_graph: self.comm_graph.clone(),
114        }
115    }
116
117    fn analyze_protocol(&mut self, protocol: &Protocol) {
118        match protocol {
119            Protocol::Send {
120                from,
121                to,
122                message,
123                continuation,
124                ..
125            } => self.analyze_send(from, to, &message.name.to_string(), continuation),
126
127            Protocol::Broadcast {
128                from,
129                to_all,
130                message,
131                continuation,
132                ..
133            } => self.analyze_broadcast(from, to_all, &message.name.to_string(), continuation),
134
135            Protocol::Choice { role, branches, .. } => self.analyze_choice(role, branches),
136            Protocol::Case { branches, .. } => {
137                for branch in branches {
138                    self.analyze_protocol(&branch.protocol);
139                }
140            }
141            Protocol::Timeout {
142                body,
143                on_timeout,
144                on_cancel,
145                ..
146            } => {
147                self.analyze_protocol(body);
148                self.analyze_protocol(on_timeout);
149                if let Some(on_cancel) = on_cancel.as_deref() {
150                    self.analyze_protocol(on_cancel);
151                }
152            }
153
154            Protocol::Loop { body, .. } => {
155                self.analyze_protocol(body);
156            }
157
158            Protocol::Parallel { protocols } => {
159                for p in protocols {
160                    self.analyze_protocol(p);
161                }
162            }
163
164            Protocol::Rec { body, .. } => {
165                self.analyze_protocol(body);
166            }
167
168            Protocol::Var(_) | Protocol::End => {}
169
170            Protocol::Begin { continuation, .. }
171            | Protocol::Await { continuation, .. }
172            | Protocol::Resolve { continuation, .. }
173            | Protocol::Invalidate { continuation, .. }
174            | Protocol::Extension { continuation, .. }
175            | Protocol::Let { continuation, .. }
176            | Protocol::Publish { continuation, .. }
177            | Protocol::PublishAuthority { continuation, .. }
178            | Protocol::Materialize { continuation, .. }
179            | Protocol::Handoff { continuation, .. }
180            | Protocol::DependentWork { continuation, .. } => {
181                self.analyze_protocol(continuation);
182            }
183        }
184    }
185
186    fn analyze_send(
187        &mut self,
188        from: &Role,
189        to: &Role,
190        message_name: &str,
191        continuation: &Protocol,
192    ) {
193        if let Some(stats) = self.role_stats.get_mut(from) {
194            stats.sends += 1;
195        }
196        if let Some(stats) = self.role_stats.get_mut(to) {
197            stats.receives += 1;
198        }
199        self.comm_graph
200            .edges
201            .push((from.clone(), to.clone(), message_name.to_string()));
202        self.analyze_protocol(continuation);
203    }
204
205    fn analyze_broadcast(
206        &mut self,
207        from: &Role,
208        to_all: &crate::ast::NonEmptyVec<Role>,
209        message_name: &str,
210        continuation: &Protocol,
211    ) {
212        if let Some(stats) = self.role_stats.get_mut(from) {
213            stats.sends += to_all.len();
214        }
215        for to in to_all {
216            if let Some(stats) = self.role_stats.get_mut(to) {
217                stats.receives += 1;
218            }
219            self.comm_graph.edges.push((
220                from.clone(),
221                to.clone(),
222                format!("{message_name} (broadcast)"),
223            ));
224        }
225        self.analyze_protocol(continuation);
226    }
227
228    fn analyze_choice(
229        &mut self,
230        role: &Role,
231        branches: &crate::ast::NonEmptyVec<crate::ast::Branch>,
232    ) {
233        if let Some(stats) = self.role_stats.get_mut(role) {
234            stats.choices += 1;
235        }
236
237        let recipients: HashSet<_> = branches
238            .iter()
239            .filter_map(|branch| match &branch.protocol {
240                Protocol::Send { to, .. } => Some(to.clone()),
241                _ => None,
242            })
243            .collect();
244        if recipients.len() > 1 {
245            self.warnings
246                .push(AnalysisWarning::AsymmetricChoice(role.clone()));
247        }
248
249        for branch in branches {
250            self.analyze_protocol(&branch.protocol);
251        }
252    }
253
254    fn check_deadlock_freedom(&self) -> bool {
255        // Simple check: ensure no circular waiting patterns
256        // More sophisticated analysis would use session type techniques
257
258        // Build dependency graph
259        let mut dependencies: HashMap<Role, HashSet<Role>> = HashMap::new();
260        for role in &self.choreography.roles {
261            dependencies.insert(role.clone(), HashSet::new());
262        }
263
264        // Analyze protocol for dependencies
265        Self::extract_dependencies(&self.choreography.protocol, &mut dependencies);
266
267        // Check for cycles using DFS
268        !has_cycle(&dependencies)
269    }
270
271    fn extract_dependencies(protocol: &Protocol, deps: &mut HashMap<Role, HashSet<Role>>) {
272        match protocol {
273            Protocol::Send {
274                from,
275                to,
276                continuation,
277                ..
278            } => {
279                if let Some(to_deps) = deps.get_mut(to) {
280                    to_deps.insert(from.clone());
281                }
282                Self::extract_dependencies(continuation, deps);
283            }
284            Protocol::Choice { branches, .. } => {
285                for branch in branches {
286                    Self::extract_dependencies(&branch.protocol, deps);
287                }
288            }
289            Protocol::Case { branches, .. } => {
290                for branch in branches {
291                    Self::extract_dependencies(&branch.protocol, deps);
292                }
293            }
294            Protocol::Timeout {
295                body,
296                on_timeout,
297                on_cancel,
298                ..
299            } => {
300                Self::extract_dependencies(body, deps);
301                Self::extract_dependencies(on_timeout, deps);
302                if let Some(on_cancel) = on_cancel.as_deref() {
303                    Self::extract_dependencies(on_cancel, deps);
304                }
305            }
306            Protocol::Loop { body, .. } => {
307                Self::extract_dependencies(body, deps);
308            }
309            Protocol::Parallel { protocols } => {
310                // Parallel branches don't create dependencies between them
311                for p in protocols {
312                    Self::extract_dependencies(p, deps);
313                }
314            }
315            Protocol::Rec { body, .. } => {
316                Self::extract_dependencies(body, deps);
317            }
318            Protocol::Broadcast { continuation, .. } => {
319                Self::extract_dependencies(continuation, deps);
320            }
321            Protocol::Var(_) | Protocol::End => {}
322
323            Protocol::Begin { continuation, .. }
324            | Protocol::Await { continuation, .. }
325            | Protocol::Resolve { continuation, .. }
326            | Protocol::Invalidate { continuation, .. }
327            | Protocol::Extension { continuation, .. }
328            | Protocol::Let { continuation, .. }
329            | Protocol::Publish { continuation, .. }
330            | Protocol::PublishAuthority { continuation, .. }
331            | Protocol::Materialize { continuation, .. }
332            | Protocol::Handoff { continuation, .. }
333            | Protocol::DependentWork { continuation, .. } => {
334                Self::extract_dependencies(continuation, deps);
335            }
336        }
337    }
338
339    fn check_progress(&self) -> bool {
340        // Check that the protocol eventually terminates or makes progress
341        Self::check_protocol_progress(&self.choreography.protocol)
342    }
343
344    fn check_protocol_progress(protocol: &Protocol) -> bool {
345        match protocol {
346            Protocol::End => true,
347            Protocol::Send { continuation, .. } => {
348                // Send is progress
349                Self::check_protocol_progress(continuation)
350            }
351            Protocol::Choice { branches, .. } => {
352                // All branches must have progress
353                branches
354                    .iter()
355                    .all(|b| Self::check_protocol_progress(&b.protocol))
356            }
357            Protocol::Case { branches, .. } => branches
358                .iter()
359                .all(|b| Self::check_protocol_progress(&b.protocol)),
360            Protocol::Timeout {
361                body,
362                on_timeout,
363                on_cancel,
364                ..
365            } => {
366                Self::check_protocol_progress(body)
367                    && Self::check_protocol_progress(on_timeout)
368                    && match on_cancel.as_deref() {
369                        Some(protocol) => Self::check_protocol_progress(protocol),
370                        None => true,
371                    }
372            }
373            Protocol::Loop { body, .. } => {
374                // Check that loop body has communication (progress)
375                has_communication(body)
376            }
377            Protocol::Parallel { protocols } => protocols.iter().all(Self::check_protocol_progress),
378            Protocol::Rec { body, .. } => {
379                // Recursive protocols must have communication
380                has_communication(body)
381            }
382            Protocol::Var(_) => true, // Assume recursive calls are okay
383            Protocol::Broadcast { continuation, .. } => Self::check_protocol_progress(continuation),
384
385            Protocol::Begin { continuation, .. }
386            | Protocol::Await { continuation, .. }
387            | Protocol::Resolve { continuation, .. }
388            | Protocol::Invalidate { continuation, .. }
389            | Protocol::Extension { continuation, .. }
390            | Protocol::Let { continuation, .. }
391            | Protocol::Publish { continuation, .. }
392            | Protocol::PublishAuthority { continuation, .. }
393            | Protocol::Materialize { continuation, .. }
394            | Protocol::Handoff { continuation, .. }
395            | Protocol::DependentWork { continuation, .. } => {
396                Self::check_protocol_progress(continuation)
397            }
398        }
399    }
400
401    fn compute_participation_info(&self) -> HashMap<Role, ParticipationInfo> {
402        let mut result = HashMap::new();
403
404        for (role, stats) in &self.role_stats {
405            result.insert(
406                role.clone(),
407                ParticipationInfo {
408                    sends: stats.sends,
409                    receives: stats.receives,
410                    choices: stats.choices,
411                    is_active: stats.sends > 0 || stats.receives > 0 || stats.choices > 0,
412                },
413            );
414        }
415
416        result
417    }
418}
419
420/// Generate a DOT graph visualization of the communication pattern
421#[must_use]
422pub fn generate_dot_graph(comm_graph: &CommunicationGraph) -> String {
423    let mut dot = String::from("digraph G {\n");
424    dot.push_str("  rankdir=LR;\n");
425    dot.push_str("  node [shape=circle];\n");
426
427    // Add nodes
428    for node in &comm_graph.nodes {
429        dot.push_str(&format!("  {};\n", node.name()));
430    }
431
432    // Add edges
433    for (from, to, label) in &comm_graph.edges {
434        dot.push_str(&format!(
435            "  {} -> {} [label=\"{}\"];\n",
436            from.name(),
437            to.name(),
438            label
439        ));
440    }
441
442    dot.push_str("}\n");
443    dot
444}