-(* Copyright (C) 2004-2005, HELM Team.
- *
- * This file is part of HELM, an Hypertextual, Electronic
- * Library of Mathematics, developed at the Computer Science
- * Department, University of Bologna, Italy.
- *
- * HELM is free software; you can redistribute it and/or
- * modify it under the terms of the GNU General Public License
- * as published by the Free Software Foundation; either version 2
- * of the License, or (at your option) any later version.
- *
- * HELM is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
- * GNU General Public License for more details.
+/* CPU control.
+ * (C) 2001, 2002, 2003, 2004 Rusty Russell
*
- * You should have received a copy of the GNU General Public License
- * along with HELM; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
- * MA 02111-1307, USA.
- *
- * For details, see the HELM World-Wide-Web page,
- * http://helm.cs.unibo.it/
- *)
-
-open Printf
-
-module Pt = CicNotationPt
-module Env = CicNotationEnv
-module Util = CicNotationUtil
-
-type pattern_id = int
-
-exception No_match
-
-module OrderedInt =
-struct
- type t = int
- let compare (x1:t) (x2:t) = Pervasives.compare x2 x1 (* reverse order *)
-end
-
-module IntSet = Set.Make (OrderedInt)
-
-let int_set_of_int_list l =
- List.fold_left (fun acc i -> IntSet.add i acc) IntSet.empty l
-
-type pattern_kind = Variable | Constructor
-type tag_t = int
-
-module type PATTERN =
-sig
- type pattern_t
- type term_t
- val classify : pattern_t -> pattern_kind
- val tag_of_pattern : pattern_t -> tag_t * pattern_t list
- val tag_of_term : term_t -> tag_t * term_t list
-end
-
-module Matcher (P: PATTERN) =
-struct
- type row_t = P.pattern_t list * P.pattern_t list * pattern_id
- type t = row_t list
-
- let compatible p1 p2 = P.classify p1 = P.classify p2
-
- let matched = List.map (fun (matched, _, pid) -> matched, pid)
-
- let partition t pidl =
- let partitions = Hashtbl.create 11 in
- let add pid row = Hashtbl.add partitions pid row in
- (try
- List.iter2 add pidl t
- with Invalid_argument _ -> assert false);
- let pidset = int_set_of_int_list pidl in
- IntSet.fold
- (fun pid acc ->
- match Hashtbl.find_all partitions pid with
- | [] -> acc
- | patterns -> (pid, List.rev patterns) :: acc)
- pidset []
-
- let are_empty t =
- match t with
- | (_, [], _) :: _ -> true
- (* if first row has an empty list of patterns, then others have as well *)
- | _ -> false
-
- (* return 2 lists of rows, first one containing homogeneous rows according
- * to "compatible" below *)
- let horizontal_split t =
- let ap, first_row, t', first_row_class =
- match t with
- | [] -> assert false
- | (_, [], _) :: _ ->
- assert false (* are_empty should have been invoked in advance *)
- | ((_, hd :: _ , _) as row) :: tl -> hd, row, tl, P.classify hd
- in
- let rec aux prev_t = function
- | [] -> List.rev prev_t, []
- | (_, [], _) :: _ -> assert false
- | ((_, hd :: _, _) as row) :: tl when compatible ap hd ->
- aux (row :: prev_t) tl
- | t -> List.rev prev_t, t
- in
- let rows1, rows2 = aux [first_row] t' in
- first_row_class, rows1, rows2
-
- (* return 2 lists, first one representing first column, second one
- * representing a new pattern matrix where matched patterns have been moved
- * to decl *)
- let vertical_split t =
- List.map
- (function
- | decls, hd :: tl, pid -> hd :: decls, tl, pid
- | _ -> assert false)
- t
-
- let variable_closure k =
- (fun matched_terms terms ->
- prerr_endline "variable_closure";
- match terms with
- | hd :: tl -> k (hd :: matched_terms) tl
- | _ -> assert false)
-
- let constructor_closure ks k =
- (fun matched_terms terms ->
- prerr_endline "constructor_closure";
- match terms with
- | t :: tl ->
- (try
- let tag, subterms = P.tag_of_term t in
- let k' = List.assoc tag ks in
- k' matched_terms (subterms @ tl)
- with Not_found -> k matched_terms terms)
- | [] -> assert false)
-
- let compiler rows match_cb fail_k =
- let rec aux t k =
- if t = [] then
- k
- else if are_empty t then
- let res = match_cb (matched t) in
- (fun matched_terms _ -> res matched_terms)
- else
- match horizontal_split t with
- | _, [], _ -> assert false
- | Variable, t', [] -> variable_closure (aux (vertical_split t') k)
- | Constructor, t', [] ->
- let tagl =
- List.map
- (function
- | _, p :: _, _ -> fst (P.tag_of_pattern p)
- | _ -> assert false)
- t'
- in
- let clusters = partition t' tagl in
- let ks =
- List.map
- (fun (tag, cluster) ->
- let cluster' =
- List.map (* add args as patterns heads *)
- (function
- | matched_p, p :: tl, pid ->
- let _, subpatterns = P.tag_of_pattern p in
- matched_p, subpatterns @ tl, pid
- | _ -> assert false)
- cluster
- in
- tag, aux cluster' k)
- clusters
- in
- constructor_closure ks k
- | _, t', t'' -> aux t' (aux t'' k)
- in
- let t = List.map (fun (p, pid) -> [], [p], pid) rows in
- let matcher = aux t (fun _ _ -> fail_k ()) in
- (fun term -> matcher [] [term])
-end
-
-module Matcher21 =
-struct
- module Pattern21 =
- struct
- type pattern_t = Pt.term
- type term_t = Pt.term
- let classify = function
- | Pt.Variable _ -> Variable
- | Pt.Magic _
- | Pt.Layout _
- | Pt.Literal _ as t ->
- prerr_endline (CicNotationPp.pp_term t);
- assert false
- | _ -> Constructor
- let tag_of_pattern = CicNotationTag.get_tag
- let tag_of_term = CicNotationTag.get_tag
- end
-
- module M = Matcher (Pattern21)
-
- let extract_magic term =
- let magic_map = ref [] in
- let add_magic m =
- let name = Util.fresh_name () in
- magic_map := (name, m) :: !magic_map;
- Pt.Variable (Pt.TermVar name)
- in
- let rec aux = function
- | Pt.AttributedTerm (_, t) -> aux t
- | Pt.Literal _
- | Pt.Layout _ -> assert false
- | Pt.Variable v -> Pt.Variable v
- | Pt.Magic m -> add_magic m
- | t -> Util.visit_ast aux t
- in
- let term' = aux term in
- term', !magic_map
-
- let env_of_matched pl tl =
- List.map2
- (fun p t ->
- match p, t with
- Pt.Variable (Pt.TermVar name), _ ->
- name, (Env.TermType, Env.TermValue t)
- | Pt.Variable (Pt.NumVar name), (Pt.Num (s, _)) ->
- name, (Env.NumType, Env.NumValue s)
- | Pt.Variable (Pt.IdentVar name), (Pt.Ident (s, None)) ->
- name, (Env.StringType, Env.StringValue s)
- | _ -> assert false)
- pl tl
-
- let rec compiler rows =
- let rows', magic_maps =
- List.split
- (List.map
- (fun (p, pid) ->
- let p', map = extract_magic p in
- (p', pid), (pid, map))
- rows)
- in
- let magichecker map =
- List.fold_left
- (fun f (name, m) ->
- let m_checker = compile_magic m in
- (fun env ->
- match m_checker (Env.lookup_term env name) env with
- | None -> None
- | Some env' -> f env'))
- (fun env -> Some env)
- map
- in
- let magichooser candidates =
- List.fold_left
- (fun f (pid, pl, checker) ->
- (fun matched_terms ->
- let env = env_of_matched pl matched_terms in
- match checker env with
- | None -> f matched_terms
- | Some env -> Some (env, pid)))
- (fun _ -> None)
- candidates
- in
- let match_cb rows =
- prerr_endline (sprintf "match_cb on %d row(s)" (List.length rows));
- let candidates =
- List.map
- (fun (pl, pid) ->
- let magic_map =
- try List.assoc pid magic_maps with Not_found -> assert false
- in
- pid, pl, magichecker magic_map)
- rows
- in
- magichooser candidates
- in
- M.compiler rows' match_cb (fun _ -> None)
-
- and compile_magic = function
- | Pt.Fold (kind, p_base, names, p_rec) ->
- let p_rec_decls = Env.declarations_of_term p_rec in
- let acc_name = try List.hd names with Failure _ -> assert false in
- let compiled = compiler [p_base, 0; p_rec, 1] in
- (fun term env ->
- let rec aux term =
- match compiled term with
- | None -> None
- | Some (env', 0) -> Some (env', [])
- | Some (env', 1) ->
- begin
- let acc = Env.lookup_term env' acc_name in
- let env'' = Env.remove env' acc_name in
- match aux acc with
- | None -> None
- | Some (base_env, rec_envl) ->
- Some (base_env, env'' :: rec_envl )
- end
- | _ -> assert false
- in
- match aux term with
- | None -> None
- | Some (base_env, rec_envl) ->
- Some (base_env @ Env.coalesce_env p_rec_decls rec_envl))
- | Pt.Default (p_some, p_none) -> (* p_none can't bound names *)
- let p_some_decls = Env.declarations_of_term p_some in
- let none_env = List.map Env.opt_binding_of_name p_some_decls in
- let compiled = compiler [p_some, 0] in
- (fun term env ->
- match compiled term with
- | None -> Some none_env
- | Some (env', 0) -> Some (List.map Env.opt_binding_some env' @ env)
- | _ -> assert false)
- | _ -> assert false
-end
-
-module Matcher32 =
-struct
- module Pattern32 =
- struct
- type cic_mask_t =
- Blob
- | Uri of string
- | Appl of cic_mask_t list
-
- let uri_of_term t = CicUtil.uri_of_term (Deannotate.deannotate_term t)
-
- let mask_of_cic = function
- | Cic.AAppl (_, tl) -> Appl (List.map (fun _ -> Blob) tl), tl
- | Cic.AConst (_, _, [])
- | Cic.AVar (_, _, [])
- | Cic.AMutInd (_, _, _, [])
- | Cic.AMutConstruct (_, _, _, _, []) as t -> Uri (uri_of_term t), []
- | _ -> Blob, []
-
- let tag_of_term t =
- let mask, tl = mask_of_cic t in
- Hashtbl.hash mask, tl
-
- let mask_of_appl_pattern = function
- | Pt.UriPattern s -> Uri s, []
- | Pt.VarPattern _ -> Blob, []
- | Pt.ApplPattern pl -> Appl (List.map (fun _ -> Blob) pl), pl
-
- let tag_of_pattern p =
- let mask, pl = mask_of_appl_pattern p in
- Hashtbl.hash mask, pl
-
- type pattern_t = Pt.cic_appl_pattern
- type term_t = Cic.annterm
-
- let classify = function
- | Pt.VarPattern _ -> Variable
- | _ -> Constructor
- end
-
- module M = Matcher (Pattern32)
-
- let compiler rows =
- let match_cb rows =
- prerr_endline (sprintf "match_cb on %d row(s)" (List.length rows));
- let pl, pid = try List.hd rows with Not_found -> assert false in
- (fun matched_terms ->
- let env =
- List.map2
- (fun p t ->
- match p with
- | Pt.VarPattern name -> name, t
- | _ -> assert false)
- pl matched_terms
- in
- Some (env, pid))
- in
- M.compiler rows match_cb (fun () -> None)
-end
-
+ * This code is licenced under the GPL.
+ */
+#include <linux/proc_fs.h>
+#include <linux/smp.h>
+#include <linux/init.h>
+#include <linux/notifier.h>
+#include <linux/sched.h>
+#include <linux/unistd.h>
+#include <linux/cpu.h>
+#include <linux/module.h>
+#include <linux/kmod.h> /* for hotplug_path */
+#include <linux/kthread.h>
+#include <linux/stop_machine.h>
+#include <asm/semaphore.h>
+
+/* This protects CPUs going up and down... */
+DECLARE_MUTEX(cpucontrol);
+
+static struct notifier_block *cpu_chain;
+
+/* Need to know about CPUs going up/down? */
+int register_cpu_notifier(struct notifier_block *nb)
+{
+ int ret;
+
+ if ((ret = down_interruptible(&cpucontrol)) != 0)
+ return ret;
+ ret = notifier_chain_register(&cpu_chain, nb);
+ up(&cpucontrol);
+ return ret;
+}
+EXPORT_SYMBOL(register_cpu_notifier);
+
+void unregister_cpu_notifier(struct notifier_block *nb)
+{
+ down(&cpucontrol);
+ notifier_chain_unregister(&cpu_chain, nb);
+ up(&cpucontrol);
+}
+EXPORT_SYMBOL(unregister_cpu_notifier);
+
+#ifdef CONFIG_HOTPLUG_CPU
+static inline void check_for_tasks(int cpu)
+{
+ struct task_struct *p;
+
+ write_lock_irq(&tasklist_lock);
+ for_each_process(p) {
+ if (task_cpu(p) == cpu && (p->utime != 0 || p->stime != 0))
+ printk(KERN_WARNING "Task %s (pid = %d) is on cpu %d\
+ (state = %ld, flags = %lx) \n",
+ p->comm, p->pid, cpu, p->state, p->flags);
+ }
+ write_unlock_irq(&tasklist_lock);
+}
+
+/* Notify userspace when a cpu event occurs, by running '/sbin/hotplug
+ * cpu' with certain environment variables set. */
+static int cpu_run_sbin_hotplug(unsigned int cpu, const char *action)
+{
+ char *argv[3], *envp[5], cpu_str[12], action_str[32];
+ int i;
+
+ sprintf(cpu_str, "CPU=%d", cpu);
+ sprintf(action_str, "ACTION=%s", action);
+ /* FIXME: Add DEVPATH. --RR */
+
+ i = 0;
+ argv[i++] = hotplug_path;
+ argv[i++] = "cpu";
+ argv[i] = NULL;
+
+ i = 0;
+ /* minimal command environment */
+ envp[i++] = "HOME=/";
+ envp[i++] = "PATH=/sbin:/bin:/usr/sbin:/usr/bin";
+ envp[i++] = cpu_str;
+ envp[i++] = action_str;
+ envp[i] = NULL;
+
+ return call_usermodehelper(argv[0], argv, envp, 0);
+}
+
+/* Take this CPU down. */
+static int take_cpu_down(void *unused)
+{
+ int err;
+
+ /* Take offline: makes arch_cpu_down somewhat easier. */
+ cpu_clear(smp_processor_id(), cpu_online_map);
+
+ /* Ensure this CPU doesn't handle any more interrupts. */
+ err = __cpu_disable();
+ if (err < 0)
+ cpu_set(smp_processor_id(), cpu_online_map);
+ else
+ /* Force idle task to run as soon as we yield: it should
+ immediately notice cpu is offline and die quickly. */
+ sched_idle_next();
+
+ return err;
+}
+
+int cpu_down(unsigned int cpu)
+{
+ int err;
+ struct task_struct *p;
+ cpumask_t old_allowed, tmp;
+
+ if ((err = lock_cpu_hotplug_interruptible()) != 0)
+ return err;
+
+ if (num_online_cpus() == 1) {
+ err = -EBUSY;
+ goto out;
+ }
+
+ if (!cpu_online(cpu)) {
+ err = -EINVAL;
+ goto out;
+ }
+
+ /* Ensure that we are not runnable on dying cpu */
+ old_allowed = current->cpus_allowed;
+ tmp = CPU_MASK_ALL;
+ cpu_clear(cpu, tmp);
+ set_cpus_allowed(current, tmp);
+
+ p = __stop_machine_run(take_cpu_down, NULL, cpu);
+ if (IS_ERR(p)) {
+ err = PTR_ERR(p);
+ goto out_allowed;
+ }
+
+ if (cpu_online(cpu))
+ goto out_thread;
+
+ /* Wait for it to sleep (leaving idle task). */
+ while (!idle_cpu(cpu))
+ yield();
+
+ /* This actually kills the CPU. */
+ __cpu_die(cpu);
+
+ /* Move it here so it can run. */
+ kthread_bind(p, smp_processor_id());
+
+ /* CPU is completely dead: tell everyone. Too late to complain. */
+ if (notifier_call_chain(&cpu_chain, CPU_DEAD, (void *)(long)cpu)
+ == NOTIFY_BAD)
+ BUG();
+
+ check_for_tasks(cpu);
+
+ cpu_run_sbin_hotplug(cpu, "offline");
+
+out_thread:
+ err = kthread_stop(p);
+out_allowed:
+ set_cpus_allowed(current, old_allowed);
+out:
+ unlock_cpu_hotplug();
+ return err;
+}
+#else
+static inline int cpu_run_sbin_hotplug(unsigned int cpu, const char *action)
+{
+ return 0;
+}
+#endif /*CONFIG_HOTPLUG_CPU*/
+
+int __devinit cpu_up(unsigned int cpu)
+{
+ int ret;
+ void *hcpu = (void *)(long)cpu;
+
+ if ((ret = down_interruptible(&cpucontrol)) != 0)
+ return ret;
+
+ if (cpu_online(cpu) || !cpu_present(cpu)) {
+ ret = -EINVAL;
+ goto out;
+ }
+ ret = notifier_call_chain(&cpu_chain, CPU_UP_PREPARE, hcpu);
+ if (ret == NOTIFY_BAD) {
+ printk("%s: attempt to bring up CPU %u failed\n",
+ __FUNCTION__, cpu);
+ ret = -EINVAL;
+ goto out_notify;
+ }
+
+ /* Arch-specific enabling code. */
+ ret = __cpu_up(cpu);
+ if (ret != 0)
+ goto out_notify;
+ if (!cpu_online(cpu))
+ BUG();
+
+ /* Now call notifier in preparation. */
+ notifier_call_chain(&cpu_chain, CPU_ONLINE, hcpu);
+
+out_notify:
+ if (ret != 0)
+ notifier_call_chain(&cpu_chain, CPU_UP_CANCELED, hcpu);
+out:
+ up(&cpucontrol);
+ return ret;
+}
projects / helm.git / commitdiff